# 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.

Proof theory

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

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.

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.

*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: doiFormally 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.

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.

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.

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: htmlMathematics 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.

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.

## 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.