Research

I am a mathematical logician and philosopher of mathematics who uses logical methods to understand mathematical language, mathematical proof, and the principles of mathematical reasoning. I am interested in applying these methods in mathematics, computer science, and philosophy.

Mathematical Logic

I was trained in the tradition of David Hilbert's Beweistheorie, or proof theory, which involves modeling mathematical reasoning in formal axiomatic systems and studying those systems in syntactic terms. My book, Mathematical Logic and Computation, tries to preserve the elements of that tradition that are still relevant to mathematics, computer science, and philosophy today.

Mathematical Logic and Computation
Cambridge University Press, 2022. Publisher's page: html.

A good deal of twentieth-century work in proof theory involved finding formal reductions of one axiomatic theory to another, showing how, for example, infinitary or nonconstructive axioms can be interpreted in finitary or computational terms. For an overview, see here:

Proof theory
Introduction to Formal Philosophy, edited by Vincent F. Hendricks and Sven Ove Hansson, Springer, 177-190, 2018. Preprint: pdf.

To that end, I have used and extended many of the standard tools, including cut elimination, normalization, realizability, functional interpretation, semantic interpretations, double-negation translations, ordinal analysis, and forcing arguments. See, for example:

Quantifier elimination for the reals with a predicate for the powers of two
Jeremy Avigad and Yimu Yin, Theoretical Computer Science, 370:48-59, 2007. Paper: doi, preprint: arXiv.
Weak theories of nonstandard arithmetic and analysis
In Stephen Simpson, editor, Reverse Mathematics 2001, A K Peters, 19-46, 2005. Preprint: pdf.
Forcing in proof theory
Bulletin of Symbolic Logic, 10:305-333, 2004. Paper: doi, jstor, bsl, preprint: pdf, erratum: html.
Eliminating definitions and Skolem functions in first-order logic
ACM Transactions on Computational Logic, 4:402-415, 2003. (Conference version: Logic in Computer Science 2001, Springer, 139-146.) Paper: doi, pdf, preprint: pdf.
Saturated models of universal theories
Annals of Pure and Applied Logic, 118:219-234, 2002. Paper: doi, preprint: pdf.
Update procedures and the 1-consistency of arithmetic
Mathematical Logic Quarterly, 48:3-13, 2002. Paper: doi, preprint: pdf.
Interpreting classical theories in constructive ones
Journal of Symbolic Logic, 65:1785-1812, 2000. Paper: jstor, euclid, preprint: pdf.
Gödel's functional ("Dialectica") interpretation
Jeremy Avigad and Solomon Feferman, in S. Buss ed., The Handbook of Proof Theory, North-Holland, 337-405, 1999. Preprint: pdf.

One of my favorite results is something of a curiosity, namely, a characterization of classical propositional logic using one connective, one axiom, and one rule:

Plausibly hard combinatorial tautologies
in Beame and Buss eds., Proof Complexity and Feasible Arithmetics, American Mathematical Society, 1-12, 1997. Preprint: pdf.

The following papers can be seen as contributions to the field of reverse mathematics, where the goal is to calibrate the axiomatic strength required to carry out common mathematical arguments:

An effective proof that open sets are Ramsey
Archive for Mathematical Logic, 37:235-240, 1998. Paper: doi, preprint: pdf.
Fundamental notions of analysis in subsystems of second-order arithmetic
Jeremy Avigad and Ksenija Simic, Annals of Pure and Applied Logic, 139:138-184, 2006. Paper: doi, preprint: pdf.
Algorithmic randomness, reverse mathematics, and the dominated convergence theorem
Jeremy Avigad, Edward Dean, and Jason Rute. Annals of Pure and Applied Logic, 163:1854-1864, 2012. Paper: doi, pdf, preprint: arXiv.

Ed Dean, John Mumma, and I have undertaken a detailed analysis of the use of diagrammatic reasoning in Euclid's Elements.

A formal system for Euclid's Elements
Jeremy Avigad, Edward Dean, and John Mumma, Review of Symbolic Logic, 2:700-768, 2009. Paper: doi, pdf. Preprint: arXiv, axioms and test data: smt, tptp, test diagram: pdf, notes and errata: html. See also Ben Northrop's code: html.

Applications of Logic to Mathematics

I have been interested in the way that logical methods can expose quantitative or computational information that is implicit in classical mathematics, in fields such as ergodic theory and dynamical systems.

Oscillation and the mean ergodic theorem for uniformly convex Banach spaces
Jeremy Avigad and Jason Rute. Ergodic Theory and Dynamical Systems, 35(4):1009-1027, 2015. Paper: pdf, preprint: arXiv.
Ultraproducts and metastability
Jeremy Avigad and José Iovino, New York Journal of Mathematics, 19:713-727, 2013. Paper: html.
Uniform distribution and algorithmic randomness
Journal of Symbolic Logic, 78:334-344, 2013. Paper: doi, pdf.
Inverting the Furstenberg correspondence
Discrete and Continuous Dynamical Systems, Series A, 32: 3421-3431, 2012. Paper: doi. preprint: arXiv.
Local stability of ergodic averages
with Jeremy Avigad, Philipp Gerhardy, and Henry Towsner, Transactions of the American Mathematical Society, 362:261-288, 2010. Paper: doi, pdf, preprint: arXiv.

The following talks provide an overview of some of that work:

Computability and uniformity in ergodic theory
Slides: pdf.
Computability, constructivity, and convergence in measure theory
Slides: pdf.

Formalization of Mathematics

Computational proof assistants now make it possible to represent mathematical definitions and theorems in digital formats that can be processed and checked mechanically. The following provide general information about the field.

Mathematics and the formal turn
Bulletin of the American Mathematical Society, 61:225-240, 2024.
Paper: doi, preprint: arXiv.
Foundations
To appear in the Handbook of Proof Assistants and their Applications in Mathematics and Computer Science, edited by Jasmin Blanchette and Assia Mahboubi, Springer. Preprint: arXiv.
The mechanization of mathematics
Notices of the AMS, 65(06):681-690, 2018. Paper: doi
Formally verified mathematics
Jeremy Avigad and John Harrison, Communications of the ACM, 57(4):66-75, 2014. Paper: doi, pdf

I have been working in the field since the early 2000s. In the fall of 2004, with some students at Carnegie Mellon, I completed a formally verified proof of the Hadamard / de la Vallée Poussin prime number theorem.

A formally verified proof of the prime number theorem
Jeremy Avigad, Kevin Donnelly, David Gray, and Paul Raff, ACM Transactions on Computational Logic, 9(1:2):1-23, 2007. Paper: doi, pdf, preprint: arXiv.

The proof scripts are still available on an otherwise outdated web page. I spent 2009-2010 academic year visiting the INRIA / Microsoft Research Joint Centre in Orsay, working on George Gonthier's project to verify the Feit-Thompson theorem.

A machine-checked proof of the odd order theorem
Georges Gonthier, Andrea Asperti, Jeremy Avigad, Yves Bertot, Cyril Cohen, François Garillot, Stéphane Le Roux, Assia Mahboubi, Russell O'Connor, Sidi Ould Biha, Ioana Pasca, Laurence Rideau, Alexey Solovyev, Enrico Tassi, Laurent Théry, in Sandrine Blazy, Christine Paulin-Mohring, and David Pichardie (eds.), Interactive Theorem Proving 2013, Springer, Berlin, pages 163-179. Paper: doi, preprint: pdf.

I did some early work in homotopy type theory and verified the central limit theorem with Johannes Hölzl and Luke Serafin.

A formally verified proof of the central limit theorem
Jeremy Avigad, Johannes Hölzl, and Luke Serafin. Journal of Automated Reasoning, 59(4):389-423, 2017. Paper: doi, online, preprint: arXiv.
Homotopy limits in type theory
Jeremy Avigad, Krzysztof Kapulkin, and Peter LeFanu Lumsdaine. Mathematical Structures in Computer Science, 25:1040-1070, 2015. Paper: pdf, Preprint: arXiv, formal proofs: github.

I have been contributing to the development of the Lean Theorem Prover since its inception. I led the development of the first libraries and documentation, and I am proud to say that a large number of my students, postdocs, and visitors have worked on it over the years. (See the fifth slide of this talk.)

The Lean mathematical library
By the mathlib Community, Certified Proofs and Programs (CPP) 2020. Paper: doi, project page: html, repository: github.
A metaprogramming framework for formal verification
Gabriel Ebner, Sebastian Ullrich, Jared Roesch, Jeremy Avigad, Leonardo de Moura, Proceedings of the ACM on Programming Languages, International Conference on Functional Programming, 1:34, 2017. Paper: doi.
The Lean theorem prover (system description)
Leonardo de Moura, Soonho Kong, Jeremy Avigad, Floris van Doorn, and Jakob von Raumer. 25th International Conference on Automated Deduction (CADE-25), Berlin, Germany, 2015. Paper: html.

See also the tutorials and documentation listed under Books, the courses and materials listed under Teaching and the Lean community web pages. Since 2021, I have been the director of the Hoskinson Center for Formal Mathematics, and our current work is described on the web pages.

I am interested in applications of formal methods to applied mathematics as well.

Verified reductions for optimization
Alexander Bentkamp, Jeremy Avigad, and Ramon Fernández Mir, in Sriram Sankaranarayanan and Natasha Sharygina, eds., Tools and Algorithms for the Construction and Analysis of Systems (TACAS) 2023, Springer, 74-92, 2023.
Paper: doi, preprint: pdf.

Formal Verification and Automated Reasoning

I am interested in automated reasoning for mathematics and formal verification.

An impossible asylum
Jeremy Avigad, Seulkee Baek, Alexander Bentkamp, Marijn Heule, and Wojciech Nawrocki, American Mathematical Monthly, 130(5):446-453, 2023. Paper: doi, preprint: arXiv.
Automated reasoning for the working mathematician
Notes: pdf, associated repository: github.
A heuristic prover for real inequalities
Jeremy Avigad, Robert Y. Lewis, and Cody Roux. Journal of Automated Reasoning, 56:367-386, 2016. (Conference version in Gerwin Klein and Ruben Gamboa, eds., Interactive Theorem Proving 2014, Springer, Heidelberg, 61-76, 2014.) Paper: doi, preprint: arXiv, code: github.

Since 2021, I have served as a consultant for StarkWare, verifying their language and library for blockchain applications.

A proof-producing compiler for blockchain applications
Jeremy Avigad, Lior Goldberg, David Levit, Yoav Seginer, and Alon Titelman,
In Adam Naumowicz and René Thiemann, eds., Interactive Theorem Proving, (ITP) 2023, Schloss Dagstuhl⁠–⁠Leibniz-Zentrum für Mathematik, 7:1-7:19, 2023. Paper: doi.
A verified algebraic representation of Cairo program execution
Jeremy Avigad, Lior Goldberg, David Levit, Yoav Seginer, and Alon Titelman, in Andrei Popescu, Steve Zdancewic, editors, Certified Proofs and Programs (CPP) 2022, 153-165. Paper: doi, preprint: arXiv.

The following papers develop a logical framework for verifying properties of systems that can be modeled with computable functions over the reals. The associated tool, dReal, is maintained by Soonho Kong and actively used at Amazon Web Services.

Delta-complete decision procedures for satisfiability over the reals
Sicun Gao, Jeremy Avigad, and Edmund M. Clarke, in Bernard Gramlich et al., International Joint Conference on Automated Reasoning (IJCAR), 286-300, 2012. Paper: doi, preprint: arxiv.
Delta-decidability over the reals
Sicun Gao, Jeremy Avigad, and Edmund M. Clarke, in Logic in Computer Science (LICS), 315-324, 2012. Paper: doi, preprint: arxiv.

Philosophy of Mathematics

I have long been interested in making sense of mathematical understanding, paying close attention to mathematical language.

What we talk about when we talk about mathematics
In Karine Chemla, José Ferreirós, Lizhen Ji, Erhard Scholz, and Chang Wang, editors, The Richness of the History of Mathematics, Springer, 651-658, 2023.
Preprint: pdf, notes on historical research: pdf.
The design of mathematical language
To appear in The Handbook of Philosophy of Mathematical Practice. Paper: Springer Link, preprint: philsci archive.
Varieties of mathematical understanding
Bulletin of the American Mathematical Society, 59:99-117, 2022. Paper: doi, preprint: arXiv.
Reliability of mathematical inference
Synthese, 198(8): 7377-7399, 2021. Paper: doi, preprint: philsci archive.
Modularity in mathematics
Review of Symbolic Logic, 13:47-79, 2020. Paper: doi, preprint: philsci archive.
Principia
An article in Aeon magazine: html
Mathematics and language
In Ernest Davis and Philip Davis eds., Mathematics, Substance, and Surmise: Views on the Meaning and Ontology of Mathematics, Springer, Cham, 235-255, 2015. Paper: SpringerLink, preprint: arXiv.
Review of Bonnie Gold and Roger A. Simons, Proof and Other Dilemmas: Mathematics and Philosophy
Notices of the American Mathematical Society, 58(11): 1580-1584, 2011. Review: pdf.
Understanding, formal verification, and the philosophy of mathematics
Journal of the Indian Council of Philosophical Research (special issue on logic and philosophy today), 27:161-197, 2010. Preprint: pdf.
Review of Marcus Giaquinto, Visual Thinking in Mathematics: An Epistemological Study
Philosophia Mathematica, 17:95-108, 2009. Review: doi, preprint: pdf.
Computers in mathematical inquiry
In Paolo Mancosu, editor, The Philosophy of Mathematical Practice, Oxford University Press, 302-316, 2008. Paper: pdf, preprint: pdf.
Understanding proofs
In Paolo Mancosu, editor, The Philosophy of Mathematical Practice, Oxford University Press, 317-353, 2008. Paper: pdf, preprint: pdf.
Mathematical method and proof
Synthese 153:105-159, 2006. Paper: doi, preprint: pdf.
Number theory and elementary arithmetic
Philosophia Mathematica, 11:257-284, 2003. Paper: doi, pdf.

This talk provides a survey overview of some of the ways I think about mathematical understanding:

Mathematical understanding
Slides: pdf

History of Mathematics

Studying the history of mathematics and seeing how it has evolved provides valuable insights into what drives the subject and how it works. I have studied nineteenth century mathematics with that aim in mind.

Character and object
Jeremy Avigad and Rebecca Morris. Review of Symbolic Logic, 9:480-510, 2016. Published version: doi, pdf, expanded version: pdf.
The concept of "character" in Dirichlet's theorem on primes in an arithmetic progression
Jeremy Avigad and Rebecca Morris. Archive for History of Exact Sciences, 68:265-326, 2014. Paper: doi, preprint: arXiv.
Methodology and metaphysics in the development of Dedekind's theory of ideals
In José Ferreirós and Jeremy Gray, editors, The Architecture of Modern Mathematics, Oxford University Press, 159-186, 2006. Uncorrected proofs: pdf, preprint: pdf.
Dedekind's 1871 version of ideal theory
translation, with an introduction; Carnegie Mellon Technical Report CMU-PHIL-162, 2004. Paper: pdf, the original: pdf.

I have also taught graduate and undergraduate seminars on the history of mathematics; see Teaching.

History of Logic

I am also interested in the history of logic and the history of the philosophy of mathematics.

Review of Eckart Menzler-Trott, Logic's Lost Genius: The Life of Gerhard Gentzen and Reinhard Kahle and Michael Rathjen, editors, Gentzen's Centenary: The Quest for Consistency
Notices of the American Mathematical Society, 63(11):1288-1292, 2016. Review: pdf.
Review of S. Barry Cooper and Jan van Leeuwen, eds., Alan Turing: His Work and Impact
Notices of the American Mathematical Society, 61(8):886-890, 2014. Review: pdf.
Computability and analysis: the legacy of Alan Turing
Jeremy Avigad and Vasco Brattka. In Rod Downey, editor, Turing's Legacy: Developments from Turing's Ideas in Logic, Cambridge University Press, 1-47, 2014. Preprint: pdf.
Gödel and the metamathematical tradition
In Charles Parsons et al. eds., Kurt Gödel: Essays for his Centennial, ASL Lecture Notes in Logic, Cambridge University Press, 45-60, 2010. Preprint: pdf.
Review of William Tait, The Provenance of Pure Reason: Essays in the Philosophy of Mathematics and its History
Bulletin of Symbolic Logic, 12:608-611, 2006. Review: bsl, preprint: pdf.
Review of Calixto Badesa, The Birth of Model Theory: Löwenheim's Theorem in the Frame of the Theory of Relatives
The Mathematical Intelligencer, 28(4):67-71, 2006. Review: doi, preprint: pdf.
Review of Dennis E. Hesseling, Gnomes in the Fog: The Reception of Brouwer's Intuitionism in the 1920s
The Mathematical Intelligencer, 28(4):71-74, 2006. Review: doi, preprint: pdf.
The epsilon calculus
Jeremy Avigad and Richard Zach, in the Stanford Encyclopedia of Philosophy. Article: html.
"Clarifying the nature of the infinite": the development of metamathematics and proof theory
Jeremy Avigad and Erich H. Reck, Carnegie Mellon Technical Report CMU-PHIL-120, 2001. Paper: pdf.