Showing 1–39 of 39 results for author: Avigad, J

Mathematics and the formal turn

Authors: Jeremy Avigad

Abstract: Since the early twentieth century, it has been understood that mathematical definitions and proofs can be represented in formal systems systems with precise grammars and rules of use. Building on such foundations, computational proof assistants now make it possible to encode mathematical knowledge in digital form. This article enumerates some of the ways that these and related technologies can hel… ▽ More Since the early twentieth century, it has been understood that mathematical definitions and proofs can be represented in formal systems systems with precise grammars and rules of use. Building on such foundations, computational proof assistants now make it possible to encode mathematical knowledge in digital form. This article enumerates some of the ways that these and related technologies can help us do mathematics. △ Less

Submitted 4 November, 2023; v1 submitted 30 October, 2023; originally announced November 2023.

MSC Class: 03B35; 68V20 (Primary) 68Q60; 68V15; 68V25; 68V35; 68T01; 97U50 (Secondary)

Varieties of mathematical understanding

Authors: Jeremy Avigad

Abstract: This essay considers ways that recent uses of computers in mathematics challenge contemporary views on the nature of mathematical understanding. It also puts these challenges in a historical perspective and offers speculation as to a possible resolution. This essay considers ways that recent uses of computers in mathematics challenge contemporary views on the nature of mathematical understanding. It also puts these challenges in a historical perspective and offers speculation as to a possible resolution. △ Less

Submitted 30 October, 2023; originally announced October 2023.

MSC Class: 00A35; 01A67 (Primary) 52-02; 52-08 (Secondary)

Journal ref: Bull. Amer. Math. Soc. 59 (2022), 99-117

ProofNet: Autoformalizing and Formally Proving Undergraduate-Level Mathematics

Authors: Zhangir Azerbayev, Bartosz Piotrowski, Hailey Schoelkopf, Edward W. Ayers, Dragomir Radev, Jeremy Avigad

Abstract: We introduce ProofNet, a benchmark for autoformalization and formal proving of undergraduate-level mathematics. The ProofNet benchmarks consists of 371 examples, each consisting of a formal theorem statement in Lean 3, a natural language theorem statement, and a natural language proof. The problems are primarily drawn from popular undergraduate pure mathematics textbooks and cover topics such as r… ▽ More We introduce ProofNet, a benchmark for autoformalization and formal proving of undergraduate-level mathematics. The ProofNet benchmarks consists of 371 examples, each consisting of a formal theorem statement in Lean 3, a natural language theorem statement, and a natural language proof. The problems are primarily drawn from popular undergraduate pure mathematics textbooks and cover topics such as real and complex analysis, linear algebra, abstract algebra, and topology. We intend for ProofNet to be a challenging benchmark that will drive progress in autoformalization and automatic theorem proving. We report baseline results on statement autoformalization via in-context learning. Moreover, we introduce two novel statement autoformalization methods: prompt retrieval and distilled backtranslation. △ Less

Submitted 23 February, 2023; originally announced February 2023.

Verified reductions for optimization

Authors: Alexander Bentkamp, Ramon Fernández Mir, Jeremy Avigad

Abstract: Numerical and symbolic methods for optimization are used extensively in engineering, industry, and finance. Various methods are used to reduce problems of interest to ones that are amenable to solution by such software. We develop a framework for designing and applying such reductions, using the Lean programming language and interactive proof assistant. Formal verification makes the process more r… ▽ More Numerical and symbolic methods for optimization are used extensively in engineering, industry, and finance. Various methods are used to reduce problems of interest to ones that are amenable to solution by such software. We develop a framework for designing and applying such reductions, using the Lean programming language and interactive proof assistant. Formal verification makes the process more reliable, and the availability of an interactive framework and ambient mathematical library provides a robust environment for constructing the reductions and reasoning about them. △ Less

Submitted 22 February, 2023; v1 submitted 23 January, 2023; originally announced January 2023.

MSC Class: 90C25; 68V15

An Impossible Asylum

Authors: Jeremy Avigad, Seulkee Baek, Alexander Bentkamp, Marijn Heule, Wojciech Nawrocki

Abstract: In 1982, Raymond Smullyan published an article, "The Asylum of Doctor Tarr and Professor Fether," that consists of a series of puzzles. These were later reprinted in the anthology, "The Lady or The Tiger? and Other Logic Puzzles." The last puzzle, which describes the asylum alluded to in the title, was designed to be especially difficult. With the help of automated reasoning, we show that the puzz… ▽ More In 1982, Raymond Smullyan published an article, "The Asylum of Doctor Tarr and Professor Fether," that consists of a series of puzzles. These were later reprinted in the anthology, "The Lady or The Tiger? and Other Logic Puzzles." The last puzzle, which describes the asylum alluded to in the title, was designed to be especially difficult. With the help of automated reasoning, we show that the puzzle's hypotheses are, in fact, inconsistent, which is to say, no such asylum can possibly exist. △ Less

Submitted 23 April, 2022; v1 submitted 3 December, 2021; originally announced December 2021.

MSC Class: 03-01 (Primary); 03B35; 68V15 (Secondary)

Verified Optimization

Authors: Alexander Bentkamp, Jeremy Avigad

Abstract: Optimization is used extensively in engineering, industry, and finance, and various methods are used to transform problems to the point where they are amenable to solution by numerical methods. We describe progress towards develo** a framework, based on the Lean interactive proof assistant, for designing and applying such reductions in reliable and flexible ways. Optimization is used extensively in engineering, industry, and finance, and various methods are used to transform problems to the point where they are amenable to solution by numerical methods. We describe progress towards develo** a framework, based on the Lean interactive proof assistant, for designing and applying such reductions in reliable and flexible ways. △ Less

Submitted 12 November, 2021; originally announced November 2021.

A verified algebraic representation of Cairo program execution

Authors: Jeremy Avigad, Lior Goldberg, David Levit, Yoav Seginer, Alon Titelman

Abstract: Cryptographic interactive proof systems provide an efficient and scalable means of verifying the results of computation on blockchain. A prover constructs a proof, off-chain, that the execution of a program on a given input terminates with a certain result. The prover then publishes a certificate that can be verified efficiently and reliably modulo commonly accepted cryptographic assumptions. The… ▽ More Cryptographic interactive proof systems provide an efficient and scalable means of verifying the results of computation on blockchain. A prover constructs a proof, off-chain, that the execution of a program on a given input terminates with a certain result. The prover then publishes a certificate that can be verified efficiently and reliably modulo commonly accepted cryptographic assumptions. The method relies on an algebraic encoding of execution traces of programs. Here we report on a verification of the correctness of such an encoding of the Cairo model of computation with respect to the STARK interactive proof system, using the Lean 3 proof assistant. △ Less

Submitted 14 December, 2021; v1 submitted 29 September, 2021; originally announced September 2021.

Foundations

Authors: Jeremy Avigad

Abstract: This is a draft of a chapter on mathematical logic and foundations for an upcoming handbook of computational proof assistants. This is a draft of a chapter on mathematical logic and foundations for an upcoming handbook of computational proof assistants. △ Less

Submitted 30 August, 2021; v1 submitted 20 September, 2020; originally announced September 2020.

Comments: For the forthcoming Handbook of Proof Assistants and Their Applications in Mathematics and Computer Science, edited by Jasmin Blanchette and Assia Mahboubi

MSC Class: 68V15 (Primary) 03-01; 03B35 (Secondary) ACM Class: F.4.1; I.2.3

Progress on a perimeter surveillance problem

Authors: Jeremy Avigad, Floris van Doorn

Abstract: We consider a perimeter surveillance problem introduced by Kingston, Beard, and Holt in 2008 and studied by Davis, Humphrey, and Kingston in 2019. In this problem, $n$ drones surveil a finite interval, moving at uniform speed and exchanging information only when they meet another drone. Kingston et al. described a particular online algorithm for coordinating their behavior and asked for an upper b… ▽ More We consider a perimeter surveillance problem introduced by Kingston, Beard, and Holt in 2008 and studied by Davis, Humphrey, and Kingston in 2019. In this problem, $n$ drones surveil a finite interval, moving at uniform speed and exchanging information only when they meet another drone. Kingston et al. described a particular online algorithm for coordinating their behavior and asked for an upper bound on how long it can take before the drones are fully synchronized. They divided the algorithm's behavior into two phases, and presented upper bounds on the length of each phase based on conjectured worst-case configurations. Davis et al. presented counterexamples to the conjecture for phase 1. We present sharp upper bounds on phase 2 which show that in this case the conjectured worst case is correct. We also present new lower bounds on phase 1 and the total time to synchronization, and report partial progress towards obtaining an upper bound. △ Less

Submitted 3 June, 2021; v1 submitted 10 August, 2020; originally announced August 2020.

MSC Class: 93A14

On the computability of graphons

Authors: Nathanael L. Ackerman, Jeremy Avigad, Cameron E. Freer, Daniel M. Roy, Jason M. Rute

Abstract: We investigate the relative computability of exchangeable binary relational data when presented in terms of the distribution of an invariant measure on graphs, or as a graphon in either $L^1$ or the cut distance. We establish basic computable equivalences, and show that $L^1$ representations contain fundamentally more computable information than the other representations, but that $0'$ suffices to… ▽ More We investigate the relative computability of exchangeable binary relational data when presented in terms of the distribution of an invariant measure on graphs, or as a graphon in either $L^1$ or the cut distance. We establish basic computable equivalences, and show that $L^1$ representations contain fundamentally more computable information than the other representations, but that $0'$ suffices to move between computable such representations. We show that $0'$ is necessary in general, but that in the case of random-free graphons, no oracle is necessary. We also provide an example of an $L^1$-computable random-free graphon that is not weakly isomorphic to any graphon with an a.e. continuous version. △ Less

Submitted 31 January, 2018; originally announced January 2018.

Comments: 24 pages, 1 figure

Proof Theory

Authors: Jeremy Avigad

Abstract: Proof theory began in the 1920's as a part of Hilbert's program, which aimed to secure the foundations of mathematics by modeling infinitary mathematics with formal axiomatic systems and proving those systems consistent using restricted, finitary means. The program thus viewed mathematics as a system of reasoning with precise linguistic norms, governed by rules that can be described and studied in… ▽ More Proof theory began in the 1920's as a part of Hilbert's program, which aimed to secure the foundations of mathematics by modeling infinitary mathematics with formal axiomatic systems and proving those systems consistent using restricted, finitary means. The program thus viewed mathematics as a system of reasoning with precise linguistic norms, governed by rules that can be described and studied in concrete terms. Today such a viewpoint has applications in mathematics, computer science, and the philosophy of mathematics. △ Less

Submitted 16 December, 2017; v1 submitted 6 November, 2017; originally announced November 2017.

Mathematics and language

Authors: Jeremy Avigad

Abstract: This essay considers the special character of mathematical reasoning, and draws on observations from interactive theorem proving and the history of mathematics to clarify the nature of formal and informal mathematical language. It proposes that we view mathematics as a system of conventions and norms that is designed to help us make sense of the world and reason efficiently. Like any designed syst… ▽ More This essay considers the special character of mathematical reasoning, and draws on observations from interactive theorem proving and the history of mathematics to clarify the nature of formal and informal mathematical language. It proposes that we view mathematics as a system of conventions and norms that is designed to help us make sense of the world and reason efficiently. Like any designed system, it can perform well or poorly, and the philosophy of mathematics has a role to play in hel** us understand the general principles by which it serves its purposes well. △ Less

Submitted 21 August, 2015; v1 submitted 27 May, 2015; originally announced May 2015.

MSC Class: 00A30

Elaboration in Dependent Type Theory

Authors: Leonardo de Moura, Jeremy Avigad, Soonho Kong, Cody Roux

Abstract: To be usable in practice, interactive theorem provers need to provide convenient and efficient means of writing expressions, definitions, and proofs. This involves inferring information that is often left implicit in an ordinary mathematical text, and resolving ambiguities in mathematical expressions. We refer to the process of passing from a quasi-formal and partially-specified expression to a co… ▽ More To be usable in practice, interactive theorem provers need to provide convenient and efficient means of writing expressions, definitions, and proofs. This involves inferring information that is often left implicit in an ordinary mathematical text, and resolving ambiguities in mathematical expressions. We refer to the process of passing from a quasi-formal and partially-specified expression to a completely precise formal one as elaboration. We describe an elaboration algorithm for dependent type theory that has been implemented in the Lean theorem prover. Lean's elaborator supports higher-order unification, type class inference, ad hoc overloading, insertion of coercions, the use of tactics, and the computational reduction of terms. The interactions between these components are subtle and complex, and the elaboration algorithm has been carefully designed to balance efficiency and usability. We describe the central design goals, and the means by which they are achieved. △ Less

Submitted 17 December, 2015; v1 submitted 16 May, 2015; originally announced May 2015.

A formally verified proof of the Central Limit Theorem

Authors: Jeremy Avigad, Johannes Hölzl, Luke Serafin

Abstract: We describe a proof of the Central Limit Theorem that has been formally verified in the Isabelle proof assistant. Our formalization builds upon and extends Isabelle's libraries for analysis and measure-theoretic probability. The proof of the theorem uses characteristic functions, which are a kind of Fourier transform, to demonstrate that, under suitable hypotheses, sums of random variables converg… ▽ More We describe a proof of the Central Limit Theorem that has been formally verified in the Isabelle proof assistant. Our formalization builds upon and extends Isabelle's libraries for analysis and measure-theoretic probability. The proof of the theorem uses characteristic functions, which are a kind of Fourier transform, to demonstrate that, under suitable hypotheses, sums of random variables converge weakly to the standard normal distribution. We also discuss the libraries and infrastructure that supported the formalization, and reflect on some of the lessons we have learned from the effort. △ Less

Submitted 1 February, 2017; v1 submitted 27 May, 2014; originally announced May 2014.

MSC Class: 60F05; 03B35 ACM Class: F.4.1; G.3

Character and object

Authors: Jeremy Avigad, Rebecca Morris

Abstract: In 1837, Dirichlet proved that there are infinitely many primes in any arithmetic progression in which the terms do not all share a common factor. Modern presentations of the proof are explicitly higher-order, in that they involve quantifying over and summing over Dirichlet characters, which are certain types of functions. The notion of a character is only implicit in Dirichlet's original proof, a… ▽ More In 1837, Dirichlet proved that there are infinitely many primes in any arithmetic progression in which the terms do not all share a common factor. Modern presentations of the proof are explicitly higher-order, in that they involve quantifying over and summing over Dirichlet characters, which are certain types of functions. The notion of a character is only implicit in Dirichlet's original proof, and the subsequent history shows a very gradual transition to the modern mode of presentation. In this essay, we describe an approach to the philosophy of mathematics in which it is an important task to understand the roles of our ontological posits and assess the extent to which they enable us to achieve our mathematical goals. We use the history of Dirichlet's theorem to understand some of the reasons that functions are treated as ordinary objects in contemporary mathematics, as well as some of the reasons one might want to resist such treatment. We also use these considerations to illuminate the formal treatment of functions and objects in Frege's logical foundation, and we argue that his philosophical and logical decisions were influenced by many of the same factors. △ Less

Submitted 21 December, 2015; v1 submitted 18 April, 2014; originally announced April 2014.

MSC Class: 01A55; 00A30; 00A35

Journal ref: The Review of Symbolic Logic 9 (2016) 480-510

A heuristic prover for real inequalities

Authors: Jeremy Avigad, Robert Y. Lewis, Cody Roux

Abstract: We describe a general method for verifying inequalities between real-valued expressions, especially the kinds of straightforward inferences that arise in interactive theorem proving. In contrast to approaches that aim to be complete with respect to a particular language or class of formulas, our method establishes claims that require heterogeneous forms of reasoning, relying on a Nelson-Oppen-styl… ▽ More We describe a general method for verifying inequalities between real-valued expressions, especially the kinds of straightforward inferences that arise in interactive theorem proving. In contrast to approaches that aim to be complete with respect to a particular language or class of formulas, our method establishes claims that require heterogeneous forms of reasoning, relying on a Nelson-Oppen-style architecture in which special-purpose modules collaborate and share information. The framework is thus modular and extensible. A prototype implementation shows that the method works well on a variety of examples, and complements techniques that are used by contemporary interactive provers. △ Less

Submitted 4 January, 2016; v1 submitted 16 April, 2014; originally announced April 2014.

ACM Class: I.1.2; G.4; F.2.1

Homotopy limits in type theory

Authors: Jeremy Avigad, Chris Kapulkin, Peter LeFanu Lumsdaine

Abstract: Working in homotopy type theory, we provide a systematic study of homotopy limits of diagrams over graphs, formalized in the Coq proof assistant. We discuss some of the challenges posed by this approach to formalizing homotopy-theoretic material. We also compare our constructions with the more classical approach to homotopy limits via fibration categories. Working in homotopy type theory, we provide a systematic study of homotopy limits of diagrams over graphs, formalized in the Coq proof assistant. We discuss some of the challenges posed by this approach to formalizing homotopy-theoretic material. We also compare our constructions with the more classical approach to homotopy limits via fibration categories. △ Less

Submitted 7 July, 2015; v1 submitted 2 April, 2013; originally announced April 2013.

Comments: 33 pages; v3: theorem numbering changed since v2 to match journal version

MSC Class: 03B70; 55U35 ACM Class: D.2.4; F.4.1

Journal ref: Math. Struct. Comp. Sci. 25 (2015) 1040-1070

Ultraproducts and metastability

Authors: Jeremy Avigad, José Iovino

Abstract: Given a convergence theorem in analysis, under very general conditions a model-theoretic compactness argument implies that there is a uniform bound on the rate of metastability. We illustrate with three examples from ergodic theory. Given a convergence theorem in analysis, under very general conditions a model-theoretic compactness argument implies that there is a uniform bound on the rate of metastability. We illustrate with three examples from ergodic theory. △ Less

Submitted 16 October, 2013; v1 submitted 14 January, 2013; originally announced January 2013.

MSC Class: 46B08; 03C20; 37A30

The concept of "character" in Dirichlet's theorem on primes in an arithmetic progression

Authors: Jeremy Avigad, Rebecca Morris

Abstract: In 1837, Dirichlet proved that there are infinitely many primes in any arithmetic progression in which the terms do not all share a common factor. We survey implicit and explicit uses of Dirichlet characters in presentations of Dirichlet's proof in the nineteenth and early twentieth centuries, with an eye towards understanding some of the pragmatic pressures that shaped the evolution of modern mat… ▽ More In 1837, Dirichlet proved that there are infinitely many primes in any arithmetic progression in which the terms do not all share a common factor. We survey implicit and explicit uses of Dirichlet characters in presentations of Dirichlet's proof in the nineteenth and early twentieth centuries, with an eye towards understanding some of the pragmatic pressures that shaped the evolution of modern mathematical method. △ Less

Submitted 26 June, 2013; v1 submitted 17 September, 2012; originally announced September 2012.

MSC Class: 01A55; 00A30; 00A35

Computability and analysis: the legacy of Alan Turing

Authors: Jeremy Avigad, Vasco Brattka

Abstract: We discuss the legacy of Alan Turing and his impact on computability and analysis. We discuss the legacy of Alan Turing and his impact on computability and analysis. △ Less

Submitted 30 October, 2012; v1 submitted 15 June, 2012; originally announced June 2012.

Comments: 49 pages

Journal ref: in Rod Downey (ed.), Turing's Legacy, Developments from Turing's Ideas in Logic, Lecture Notes in Logic 42, Cambridge University Press 2014, p. 1-47

Delta-Decidability over the Reals

Authors: Sicun Gao, Jeremy Avigad, Edmund Clarke

Abstract: Given any collection F of computable functions over the reals, we show that there exists an algorithm that, given any L_F-sentence \varphi containing only bounded quantifiers, and any positive rational number δ, decides either "\varphi is true", or "a δ-strengthening of \varphi is false". Under mild assumptions, for a C-computable signature F, the δ-decision problem for bounded Σ_k-sentences in L_… ▽ More Given any collection F of computable functions over the reals, we show that there exists an algorithm that, given any L_F-sentence \varphi containing only bounded quantifiers, and any positive rational number δ, decides either "\varphi is true", or "a δ-strengthening of \varphi is false". Under mild assumptions, for a C-computable signature F, the δ-decision problem for bounded Σ_k-sentences in L_F resides in (Σ_k^P)^C. The results stand in sharp contrast to the well-known undecidability results, and serve as a theoretical basis for the use of numerical methods in decision procedures for nonlinear first-order theories over the reals. △ Less

Submitted 30 April, 2012; originally announced April 2012.

Comments: A short version appears in LICS 2012

Delta-Complete Decision Procedures for Satisfiability over the Reals

Authors: Sicun Gao, Jeremy Avigad, Edmund Clarke

Abstract: We introduce the notion of "δ-complete decision procedures" for solving SMT problems over the real numbers, with the aim of handling a wide range of nonlinear functions including transcendental functions and solutions of Lipschitz-continuous ODEs. Given an SMT problem \varphi and a positive rational number δ, a δ-complete decision procedure determines either that \varphi is unsatisfiable, or that… ▽ More We introduce the notion of "δ-complete decision procedures" for solving SMT problems over the real numbers, with the aim of handling a wide range of nonlinear functions including transcendental functions and solutions of Lipschitz-continuous ODEs. Given an SMT problem \varphi and a positive rational number δ, a δ-complete decision procedure determines either that \varphi is unsatisfiable, or that the "δ-weakening" of \varphi is satisfiable. Here, the δ-weakening of \varphi is a variant of \varphi that allows δ-bounded numerical perturbations on \varphi. We prove the existence of δ-complete decision procedures for bounded SMT over reals with functions mentioned above. For functions in Type 2 complexity class C, under mild assumptions, the bounded δ-SMT problem is in NP^C. δ-Complete decision procedures can exploit scalable numerical methods for handling nonlinearity, and we propose to use this notion as an ideal requirement for numerically-driven decision procedures. As a concrete example, we formally analyze the DPLL<ICP> framework, which integrates Interval Constraint Propagation (ICP) in DPLL(T), and establish necessary and sufficient conditions for its δ-completeness. We discuss practical applications of δ-complete decision procedures for correctness-critical applications including formal verification and theorem proving. △ Less

Submitted 17 September, 2012; v1 submitted 16 April, 2012; originally announced April 2012.

Comments: A shorter version appears in IJCAR 2012

Uniform distribution and algorithmic randomness

Authors: Jeremy Avigad

Abstract: A seminal theorem due to Weyl states that if (a_n) is any sequence of distinct integers, then, for almost every real number x, the sequence (a_n x) is uniformly distributed modulo one. In particular, for almost every x in the unit interval, the sequence (a_n x) is uniformly distributed modulo one for every computable sequence (a_n) of distinct integers. Call such an x "UD random". Here it is shown… ▽ More A seminal theorem due to Weyl states that if (a_n) is any sequence of distinct integers, then, for almost every real number x, the sequence (a_n x) is uniformly distributed modulo one. In particular, for almost every x in the unit interval, the sequence (a_n x) is uniformly distributed modulo one for every computable sequence (a_n) of distinct integers. Call such an x "UD random". Here it is shown that every Schnorr random real is UD random, but there are Kurtz random reals that are not UD random. On the other hand, Weyl's theorem still holds relative to a particular effectively closed null set, so there are UD random reals that are not Kurtz random. △ Less

Submitted 14 July, 2012; v1 submitted 19 March, 2012; originally announced March 2012.

MSC Class: 03D32; 11K06

Oscillation and the mean ergodic theorem for uniformly convex Banach spaces

Authors: Jeremy Avigad, Jason Rute

Abstract: Let B be a p-uniformly convex Banach space, with p >= 2. Let T be a linear operator on B, and let A_n x denote the ergodic average (1 / n) sum_{i< n} T^n x. We prove the following variational inequality in the case where T is power bounded from above and below: for any increasing sequence (t_k)_{k in N} of natural numbers we have sum_k || A_{t_{k+1}} x - A_{t_k} x ||^p <= C || x ||^p, where the co… ▽ More Let B be a p-uniformly convex Banach space, with p >= 2. Let T be a linear operator on B, and let A_n x denote the ergodic average (1 / n) sum_{i< n} T^n x. We prove the following variational inequality in the case where T is power bounded from above and below: for any increasing sequence (t_k)_{k in N} of natural numbers we have sum_k || A_{t_{k+1}} x - A_{t_k} x ||^p <= C || x ||^p, where the constant C depends only on p and the modulus of uniform convexity. For T a nonexpansive operator, we obtain a weaker bound on the number of epsilon-fluctuations in the sequence. We clarify the relationship between bounds on the number of epsilon-fluctuations in a sequence and bounds on the rate of metastability, and provide lower bounds on the rate of metastability that show that our main result is sharp. △ Less

Submitted 26 August, 2013; v1 submitted 19 March, 2012; originally announced March 2012.

MSC Class: 37A30; 03F60

Journal ref: Ergod. Th. Dynam. Sys. 35 (2014) 1009-1027

Type inference in mathematics

Authors: Jeremy Avigad

Abstract: In the theory of programming languages, type inference is the process of inferring the type of an expression automatically, often making use of information from the context in which the expression appears. Such mechanisms turn out to be extremely useful in the practice of interactive theorem proving, whereby users interact with a computational proof assistant to construct formal axiomatic derivati… ▽ More In the theory of programming languages, type inference is the process of inferring the type of an expression automatically, often making use of information from the context in which the expression appears. Such mechanisms turn out to be extremely useful in the practice of interactive theorem proving, whereby users interact with a computational proof assistant to construct formal axiomatic derivations of mathematical theorems. This article explains some of the mechanisms for type inference used by the Mathematical Components project, which is working towards a verification of the Feit-Thompson theorem. △ Less

Submitted 9 May, 2012; v1 submitted 24 November, 2011; originally announced November 2011.

ACM Class: F.4.1; I.2.3

Metastable convergence theorems

Authors: Jeremy Avigad, Edward Dean, Jason Rute

Abstract: The dominated convergence theorem implies that if (f_n) is a sequence of functions on a probability space taking values in the interval [0,1], and (f_n) converges pointwise a.e., then the sequence of integrals converges to the integral of the pointwise limit. Tao has proved a quantitative version of this theorem: given a uniform bound on the rates of metastable convergence in the hypothesis, there… ▽ More The dominated convergence theorem implies that if (f_n) is a sequence of functions on a probability space taking values in the interval [0,1], and (f_n) converges pointwise a.e., then the sequence of integrals converges to the integral of the pointwise limit. Tao has proved a quantitative version of this theorem: given a uniform bound on the rates of metastable convergence in the hypothesis, there is a bound on the rate of metastable convergence in the conclusion that is independent of the sequence (f_n) and the underlying space. We prove a slight strengthening of Tao's theorem which, moreover, provides an explicit description of the second bound in terms of the first. Specifically, we show that when the first bound is given by a continuous functional, the bound in the conclusion can be computed by a recursion along the tree of unsecured sequences. We also establish a quantitative version of Egorov's theorem, and introduce a new mode of convergence related to these notions. △ Less

Submitted 22 August, 2011; originally announced August 2011.

MSC Class: 28A20; 03F60

Journal ref: Journal of Logic & Analysis 4:3 (2012) 1-19

Algorithmic randomness, reverse mathematics, and the dominated convergence theorem

Authors: Jeremy Avigad, Edward Dean, Jason Rute

Abstract: We analyze the pointwise convergence of a sequence of computable elements of L^1(2^omega) in terms of algorithmic randomness. We consider two ways of expressing the dominated convergence theorem and show that, over the base theory RCA_0, each is equivalent to the assertion that every G_delta subset of Cantor space with positive measure has an element. This last statement is, in turn, equivalent to… ▽ More We analyze the pointwise convergence of a sequence of computable elements of L^1(2^omega) in terms of algorithmic randomness. We consider two ways of expressing the dominated convergence theorem and show that, over the base theory RCA_0, each is equivalent to the assertion that every G_delta subset of Cantor space with positive measure has an element. This last statement is, in turn, equivalent to weak weak König's lemma relativized to the Turing jump of any set. It is also equivalent to the conjunction of the statement asserting the existence of a 2-random relative to any given set and the principle of Sigma_2 collection. △ Less

Submitted 9 May, 2012; v1 submitted 3 June, 2011; originally announced June 2011.

MSC Class: 03B30; 03D32; 03F60

Journal ref: Annals of Pure and Applied Logic 163 (2012) 1854-1864

Uncomputably noisy ergodic limits

Authors: Jeremy Avigad

Abstract: V'yugin has shown that there are a computable shift-invariant measure on Cantor space and a simple function f such that there is no computable bound on the rate of convergence of the ergodic averages A_n f. Here it is shown that in fact one can construct an example with the property that there is no computable bound on the complexity of the limit; that is, there is no computable bound on how compl… ▽ More V'yugin has shown that there are a computable shift-invariant measure on Cantor space and a simple function f such that there is no computable bound on the rate of convergence of the ergodic averages A_n f. Here it is shown that in fact one can construct an example with the property that there is no computable bound on the complexity of the limit; that is, there is no computable bound on how complex a simple function needs to be to approximate the limit to within a given epsilon. △ Less

Submitted 31 October, 2011; v1 submitted 3 May, 2011; originally announced May 2011.

MSC Class: 03F60; 37A25

Journal ref: Notre Dame J. Formal Logic 53, no. 3 (2012), 347-350

Inverting the Furstenberg correspondence

Authors: Jeremy Avigad

Abstract: Given a sequence of subsets A_n of {0,...,n-1}, the Furstenberg correspondence principle provides a shift-invariant measure on Cantor space that encodes combinatorial information about infinitely many of the A_n's. Here it is shown that this process can be inverted, so that for any such measure there are finite sets whose combinatorial properties approximate it arbitarily well. Moreover, we obtain… ▽ More Given a sequence of subsets A_n of {0,...,n-1}, the Furstenberg correspondence principle provides a shift-invariant measure on Cantor space that encodes combinatorial information about infinitely many of the A_n's. Here it is shown that this process can be inverted, so that for any such measure there are finite sets whose combinatorial properties approximate it arbitarily well. Moreover, we obtain an explicit upper bound on how large n has to be to obtain a sufficiently good approximation. As a consequence of the inversion theorem, we show that every computable invariant measure on Cantor space has a computable generic point. We also present a generalization of the correspondence principle and its inverse to countable discrete amenable groups. △ Less

Submitted 1 February, 2012; v1 submitted 3 January, 2011; originally announced January 2011.

MSC Class: 37A45; 03F60

Metastability in the Furstenberg-Zimmer tower

Authors: Jeremy Avigad, Henry Towsner

Abstract: According to the Furstenberg-Zimmer structure theorem, every measure-preserving system has a maximal distal factor, and is weak mixing relative to that factor. Furstenberg and Katznelson used this structural analysis of measure-preserving systems to provide a perspicuous proof of Szemerédi's theorem. Beleznay and Foreman showed that, in general, the transfinite construction of the maximal distal f… ▽ More According to the Furstenberg-Zimmer structure theorem, every measure-preserving system has a maximal distal factor, and is weak mixing relative to that factor. Furstenberg and Katznelson used this structural analysis of measure-preserving systems to provide a perspicuous proof of Szemerédi's theorem. Beleznay and Foreman showed that, in general, the transfinite construction of the maximal distal factor of a separable measure-preserving system can extend arbitrarily far into the countable ordinals. Here we show that the Furstenberg-Katznelson proof does not require the full strength of the maximal distal factor, in the sense that the proof only depends on a combinatorial weakening of its properties. We show that this combinatorially weaker property obtains fairly low in the transfinite construction, namely, by the $ω^{ω^ω}$th level. △ Less

Submitted 16 June, 2010; v1 submitted 2 February, 2009; originally announced February 2009.

MSC Class: 37A25; 37A45; 03F03

The computational content of classical arithmetic

Authors: Jeremy Avigad

Abstract: Almost from the inception of Hilbert's program, foundational and structural efforts in proof theory have been directed towards the goal of clarifying the computational content of modern mathematical methods. This essay surveys various methods of extracting computational information from proofs in classical first-order arithmetic, and reflects on some of the relationships between them. Variants of… ▽ More Almost from the inception of Hilbert's program, foundational and structural efforts in proof theory have been directed towards the goal of clarifying the computational content of modern mathematical methods. This essay surveys various methods of extracting computational information from proofs in classical first-order arithmetic, and reflects on some of the relationships between them. Variants of the Gödel-Gentzen double-negation translation, some not so well known, serve to provide canonical and efficient computational interpretations of that theory. △ Less

Submitted 16 June, 2010; v1 submitted 16 January, 2009; originally announced January 2009.

MSC Class: 03F30; 03F10; 03F50

A formal system for Euclid's Elements

Authors: Jeremy Avigad, Edward Dean, John Mumma

Abstract: We present a formal system, E, which provides a faithful model of the proofs in Euclid's Elements, including the use of diagrammatic reasoning. We present a formal system, E, which provides a faithful model of the proofs in Euclid's Elements, including the use of diagrammatic reasoning. △ Less

Submitted 4 May, 2009; v1 submitted 23 October, 2008; originally announced October 2008.

MSC Class: 03B30; 51M05; 03B35

Journal ref: Review of Symbolic Logic 2:4 (2009) 700-768

A language for mathematical knowledge management

Authors: Steven Kieffer, Jeremy Avigad, Harvey Friedman

Abstract: We argue that the language of Zermelo Fraenkel set theory with definitions and partial functions provides the most promising bedrock semantics for communicating and sharing mathematical knowledge. We then describe a syntactic sugaring of that language that provides a way of writing remarkably readable assertions without straying far from the set-theoretic semantics. We illustrate with some example… ▽ More We argue that the language of Zermelo Fraenkel set theory with definitions and partial functions provides the most promising bedrock semantics for communicating and sharing mathematical knowledge. We then describe a syntactic sugaring of that language that provides a way of writing remarkably readable assertions without straying far from the set-theoretic semantics. We illustrate with some examples of formalized textbook definitions from elementary set theory and point-set topology. We also present statistics concerning the complexity of these definitions, under various complexity measures. △ Less

Submitted 3 January, 2011; v1 submitted 9 May, 2008; originally announced May 2008.

ACM Class: F.4.1; I.2.4

Journal ref: Studies in Logic, Grammar and Rhetoric, 18:51-66, 2009

Functional interpretation and inductive definitions

Authors: Jeremy Avigad, Henry Towsner

Abstract: Extending Gödel's \emph{Dialectica} interpretation, we provide a functional interpretation of classical theories of positive arithmetic inductive definitions, reducing them to theories of finite-type functionals defined using transfinite recursion on well-founded trees. Extending Gödel's \emph{Dialectica} interpretation, we provide a functional interpretation of classical theories of positive arithmetic inductive definitions, reducing them to theories of finite-type functionals defined using transfinite recursion on well-founded trees. △ Less

Submitted 17 February, 2009; v1 submitted 13 February, 2008; originally announced February 2008.

Comments: minor corrections and changes

MSC Class: 03F25; 03F10; 03D70

Local stability of ergodic averages

Authors: Jeremy Avigad, Philipp Gerhardy, Henry Towsner

Abstract: The mean ergodic theorem is equivalent to the assertion that for every function K and every epsilon, there is an n with the property that the ergodic averages A_m f are stable to within epsilon on the interval [n,K(n)]. We show that even though it is not generally possible to compute a bound on the rate of convergence of a sequence of ergodic averages, one can give explicit bounds on n in terms… ▽ More The mean ergodic theorem is equivalent to the assertion that for every function K and every epsilon, there is an n with the property that the ergodic averages A_m f are stable to within epsilon on the interval [n,K(n)]. We show that even though it is not generally possible to compute a bound on the rate of convergence of a sequence of ergodic averages, one can give explicit bounds on n in terms of K and || f || / epsilon. This tells us how far one has to search to find an n so that the ergodic averages are "locally stable" on a large interval. We use these bounds to obtain a similarly explicit version of the pointwise ergodic theorem, and show that our bounds are qualitatively different from ones that can be obtained using upcrossing inequalities due to Bishop and Ivanov. Finally, we explain how our positive results can be viewed as an application of a body of general proof-theoretic methods falling under the heading of "proof mining." △ Less

Submitted 9 May, 2008; v1 submitted 11 June, 2007; originally announced June 2007.

Comments: Minor errors corrected. To appear in Transactions of the AMS

MSC Class: 37A30; 03F60; 03F03

Journal ref: Trans. Amer. Math. Soc. 362 (2010), 261-288

A decision procedure for linear "big O" equations

Authors: Jeremy Avigad, Kevin Donnelly

Abstract: Let $F$ be the set of functions from an infinite set, $S$, to an ordered ring, $R$. For $f$, $g$, and $h$ in $F$, the assertion $f = g + O(h)$ means that for some constant $C$, $|f(x) - g(x)| \leq C |h(x)|$ for every $x$ in $S$. Let $L$ be the first-order language with variables ranging over such functions, symbols for $0, +, -, \min, \max$, and absolute value, and a ternary relation… ▽ More Let $F$ be the set of functions from an infinite set, $S$, to an ordered ring, $R$. For $f$, $g$, and $h$ in $F$, the assertion $f = g + O(h)$ means that for some constant $C$, $|f(x) - g(x)| \leq C |h(x)|$ for every $x$ in $S$. Let $L$ be the first-order language with variables ranging over such functions, symbols for $0, +, -, \min, \max$, and absolute value, and a ternary relation $f = g + O(h)$. We show that the set of quantifier-free formulas in this language that are valid in the intended class of interpretations is decidable, and does not depend on the underlying set, $S$, or the ordered ring, $R$. If $R$ is a subfield of the real numbers, we can add a constant 1 function, as well as multiplication by constants from any computable subfield. We obtain further decidability results for certain situations in which one adds symbols denoting the elements of a fixed sequence of functions of strictly increasing rates of growth. △ Less

Submitted 10 January, 2007; originally announced January 2007.

ACM Class: F.4.1; I.2.3

Quantifier elimination for the reals with a predicate for the powers of two

Authors: Jeremy Avigad, Yimu Yin

Abstract: In 1985, van den Dries showed that the theory of the reals with a predicate for the integer powers of two admits quantifier elimination in an expanded language, and is hence decidable. He gave a model-theoretic argument, which provides no apparent bounds on the complexity of a decision procedure. We provide a syntactic argument that yields a procedure that is primitive recursive, although not el… ▽ More In 1985, van den Dries showed that the theory of the reals with a predicate for the integer powers of two admits quantifier elimination in an expanded language, and is hence decidable. He gave a model-theoretic argument, which provides no apparent bounds on the complexity of a decision procedure. We provide a syntactic argument that yields a procedure that is primitive recursive, although not elementary. In particular, we show that it is possible to eliminate a single block of existential quantifiers in time $2^0_{O(n)}$, where $n$ is the length of the input formula and $2_k^x$ denotes $k$-fold iterated exponentiation. △ Less

Submitted 19 October, 2006; originally announced October 2006.

ACM Class: F.4.1; I.2.3

Combining decision procedures for the reals

Authors: Jeremy Avigad, Harvey Friedman

Abstract: <p>We address the general problem of determining the validity of boolean combinations of equalities and inequalities between real-valued expressions. In particular, we consider methods of establishing such assertions using only restricted forms of distributivity. At the same time, we explore ways in which "local" decision or heuristic procedures for fragments of the theory of the reals can be am… ▽ More <p>We address the general problem of determining the validity of boolean combinations of equalities and inequalities between real-valued expressions. In particular, we consider methods of establishing such assertions using only restricted forms of distributivity. At the same time, we explore ways in which "local" decision or heuristic procedures for fragments of the theory of the reals can be amalgamated into global ones. </p> <p>Let <em>Tadd[Q]</em> be the first-order theory of the real numbers in the language of ordered groups, with negation, a constant <em>1</em>, and function symbols for multiplication by rational constants. Let <em>Tmult[Q]</em> be the analogous theory for the multiplicative structure, and let <em>T[Q]</em> be the union of the two. We show that although <em>T[Q]</em> is undecidable, the universal fragment of <em>T[Q]</em> is decidable. We also show that terms of <em>T[Q]</em>can fruitfully be put in a normal form. We prove analogous results for theories in which <em>Q</em> is replaced, more generally, by suitable subfields <em>F</em> of the reals. Finally, we consider practical methods of establishing quantifier-free validities that approximate our (impractical) decidability results.</p> △ Less

Submitted 18 October, 2006; v1 submitted 31 January, 2006; originally announced January 2006.

Comments: Will appear in Logical Methods in Computer Science

ACM Class: F.4.1; I.2.3

Journal ref: Logical Methods in Computer Science, Volume 2, Issue 4 (October 18, 2006) lmcs:2240

A formally verified proof of the prime number theorem

Authors: Jeremy Avigad, Kevin Donnelly, David Gray, Paul Raff

Abstract: The prime number theorem, established by Hadamard and de la Vall'ee Poussin independently in 1896, asserts that the density of primes in the positive integers is asymptotic to 1 / ln x. Whereas their proofs made serious use of the methods of complex analysis, elementary proofs were provided by Selberg and Erd"os in 1948. We describe a formally verified version of Selberg's proof, obtained using… ▽ More The prime number theorem, established by Hadamard and de la Vall'ee Poussin independently in 1896, asserts that the density of primes in the positive integers is asymptotic to 1 / ln x. Whereas their proofs made serious use of the methods of complex analysis, elementary proofs were provided by Selberg and Erd"os in 1948. We describe a formally verified version of Selberg's proof, obtained using the Isabelle proof assistant. △ Less

Submitted 6 April, 2006; v1 submitted 9 September, 2005; originally announced September 2005.

Comments: 23 pages

ACM Class: F.4.1; I.2.3