Papers
This list includes research articles, surveys, expository articles, unpublished notes, and a translation. Some of these papers are also listed, arranged by subject matter, under Research. See also listings on MathSciNet, Zentralblatt, Google Scholar, and DBLP.
Anatomy of a formal proof
Jeremy Avigad, Johan Commelin, Heather Macbeth, and Adam Topaz
Preprint: arXiv.ImProver: Agent-based automated proof optimization
Riyaz Ahuja, Jeremy Avigad, Prasad Tetali, and Sean Welleck.
Preprint: arXiv.Verified substitution redundancy checking
Cayden Codel, Jeremy Avigad, and Marijn Heule.
To appear in Formal Methods in Computer-Aided Design (FMCAD) 2024. Preprint: pdf.Duper: A proof-producing superposition theorem prover for dependent type theory
Joshua Clune, Yicheng Qian, Jeremy Avigad, and Alexander Bentkamp.
Interactive Theorem Proving (ITP) 2024. Paper: doi.Automated reasoning for mathematics
Jeremy Avigad.
International Joint Conference on Automated Reasoning (IJCAR) 2024. Paper: doi.Verified encodings for SAT Solvers
Cayden Codel, Jeremy Avigad, and Marijn Heule.
In A. Nadel and K. Y. Rozier, eds., Formal Methods in Computer Aided Design (FMCAD) 2023, TU Wien Academic Press, 141-151. Paper: doi.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.Certified knowledge compilation with application to verified model counting
Randal Bryant, Wojciech Nawrocki, Jeremy Avigad, and Marijn Heule.
In Meena Mahajan and Friedrich Slivovsky, eds., Theory and Applications of Satisfiabilty Testing (SAT) 2023, Schloss Dagstuhl–Leibniz-Zentrum für Mathematik, 6:1-6:20, 2023.
Paper: doi.Mathematics and the formal turn
Jeremy Avigad.
Bulletin of the American Mathematical Society, 61:225-240, 2024.
Paper: doi, preprint: arXiv.ProofNet: A benchmark for autoformalizing and formally proving undergraduate-level mathematics problems
Zhangir Azerbayev, Bartosz Piotrowski, Hailey Schoelkopf, Edward W. Ayers, Dragomir Radev, and Jeremy Avigad.
Preprint: arXiv.Verified reductions for optimization
Alexander Bentkamp, Ramon Fernández Mir, and Jeremy Avigad.
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.What we talk about when we talk about mathematics
Jeremy Avigad.
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.
Paper: doi, preprint: pdf, notes on historical research: pdf.Two-sorted Frege arithmetic is not conservative
Stephen Mackereth and Jeremy Avigad.
Review of Symbolic Logic, 16(4):1199-1232, 2023.
Paper: doi.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.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 design of mathematical language
Jeremy Avigad.
In Bharath Sriraman, editor, The Handbook of Philosophy of Mathematical Practice, Springer, 3151-3189, 2024.
Paper: Springer Link, preprint: philsci archive.Verified optimization (work in progress)
Alexander Bentkamp and Jeremy Avigad.
Formal Methods for Mathematics 2021.
Paper: pdf, preprint: arXiv.Varieties of mathematical understanding
Jeremy Avigad.
Bulletin of the American Mathematical Society, 59:99-117, 2022.
Paper: doi, preprint: arXiv.Foundations
Jeremy Avigad.
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.Progress on a perimeter surveillance problem
Jeremy Avigad and Floris van Doorn.
IEEE International Conference on Autonomous Systems (ICAS) 2021.
Paper: pdf, preprint (longer version): arXiv.The Lean mathematical library
The mathlib Community
In Jasmin Blanchette and Cătălin Hritcu, editors, Certified Proofs and Programs (CPP) 2020, ACM Publications, 2020.
Paper: doi.Reliability of mathematical inference
Jeremy Avigad.
Synthese, 198(8): 7377-7399, 2021.
Paper: doi, preprint: philsci archive.Automated reasoning for the working mathematician
Jeremy Avigad.
Notes: pdf, associated repository: github.A formalization of the mutilated chessboard theorem
Jeremy Avigad.
Notes: pdf.Quotients of polynomial functors
Jeremy Avigad, Mario Carneiro, and Simon Hudon.
In John Harrison, John O'Leary, and Andrew Tolmach, editors, Interactive Theorem Proving (ITP) 2019, LIPIcs, 6:1-6:19, 2019.
Paper: doi.Algorithmic barriers to representing conditional independence
Nathanael L. Ackerman, Jeremy Avigad, Cameron E. Freer, Daniel M. Roy, Jason M. Rute.
Logic in Computer Science (LICS) 2019.
Paper: doi.Principia
Jeremy Avigad.
Aeon magazine: html.Learning logic and proof with an interactive theorem prover
Jeremy Avigad.
In Gila Hanna, David Reid, and Michael de Viliers, Proof Technology in Mathematics Research and Teaching, Springer, Cham, 277-290, 2019.
Preprint: pdf.The mechanization of mathematics
Jeremy Avigad.
Notices of the AMS, 65(06):681-690, 2018. Reprinted in Mircea Pitici editor, The Best Writing on Mathematics 2019, Princeton University Press, 2019, 150-170.
Paper: doi.Introduction to Milestones in Interactive Theorem Proving
Jeremy Avigad, Jasmin Christian Blanchette, Gerwin Klein, Lawrence Paulson, Andrei Popescu, and Gregor Snelting.
Journal of Automated Reasoning, 61:1-8, 2018.
Paper: doi, preprint: pdf.A metaprogramming framework for formal verification
Gabriel Ebner, Sebastian Ullrich, Jared Roesch, Jeremy Avigad and Leonardo de Moura.
Proceedings of the ACM on Programming Languages, International Conference on Functional Programming 2017, 1:34, 2017.
Paper: doi.Modularity in mathematics
Jeremy Avigad.
Review of Symbolic Logic, 13:47-79, 2020.
Paper: doi, preprint: philsci archive.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.Elaboration in dependent type theory
Jeremy Avigad, Leonardo de Moura, Soonho Kong, and Cody Roux.
Unpublished: pdf.The Lean theorem prover (system description)
Jeremy Avigad, Leonardo de Moura, Soonho Kong, Floris van Doorn, and Jakob von Raumer.
25th International Conference on Automated Deduction (CADE-25), Berlin, Germany, 2015.
Paper: pdf.Mathematics and language
Jeremy Avigad.
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.Character and object
Jeremy Avigad and Rebecca Morris.
Review of Symbolic Logic, 9:480-510, 2016.
Published version: doi, pdf. Expanded version: pdf.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.Formally verified mathematics
Jeremy Avigad and John Harrison.
Communications of the ACM, 57(4):66-75, 2014.
Paper: doi, pdf.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.Homotopy limits in type theory
Jeremy Avigad, Krzysztof Kapulkin, and Peter LeFanu Lumsdaine.
Mathematical Structures in Computer Science, 25:1040-1070, 2015. Paper: pdf, prerint: arXiv, code: github.Ultraproducts and metastability
Jeremy Avigad and José Iovino
New York Journal of Mathematics, 19:713-727, 2013. Paper: html.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.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.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.Uniform distribution and algorithmic randomness
Jeremy Avigad.
Journal of Symbolic Logic, 78:334-344, 2013.
Paper: doi, reprint: pdf, preprint: arXiv.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.
Logic in Computer Science (LICS), 315-324, 2012.
Paper: doi, preprint: arxiv.Type inference in mathematics
Jeremy Avigad.
Bulletin of the European Association for Theoretical Computer Science, 106:78-98, 2012.
Paper: journal, preprint: arXiv.A metastable dominated convergence theorem
Jeremy Avigad, Edward Dean, and Jason Rute.
Journal of Logic and Analysis, 4:3:1-19, 2012.
Paper: doi.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, reprint: pdf, preprint: arXiv.Uncomputably noisy ergodic limits
Jeremy Avigad.
Notre Dame Journal of Formal Logic, 53:347-350, 2012.
Paper: doi, preprint: arXiv.Inverting the Furstenberg correspondence
Jeremy Avigad.
Discrete and Continuous Dynamical Systems, Series A, 32:3421-3431, 2012.
Paper: doi, preprint: arXiv.Zen and the art of formalization
Andrea Asperti and Jeremy Avigad.
Mathematical Structures in Computer Science (special issue on interactive theorem proving and the formalization of mathematics), 21:679-682, 2011.
Paper: doi, preprint: pdf.Proof theory
Jeremy Avigad.
Introduction to Formal Philosophy, edited by Vincent F. Hendricks and Sven Ove Hansson, Springer, 177-190, 2018.
Preprint: pdf.Understanding, formal verification, and the philosophy of mathematics
Jeremy Avigad.
Journal of the Indian Council of Philosophical Research (special issue on logic and philosophy today), 27:161-197, 2010.
Preprint: pdf.Building a push-button RESOLVE verifier: Progress and challenges
with Murali Sitaraman (first author) and many others.
Formal Aspects of Computing, 23:607-626, 2011.
Paper: doi.Metastability in the Furstenberg-Zimmer tower
Jeremy Avigad and Henry Towsner.
Fundamenta Mathematicae, 210:243-268, 2010.
Paper: journal, preprint: arXiv.The computational content of classical arithmetic
Jeremy Avigad.
In Solomon Feferman and Wilfried Sieg, eds., Proofs, Categories, and Computations: Essays in Honor of Grigori Mints, College Publications, 15-30, 2010.
Preprint: arXiv.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, Ben Northrop's code: html.A language for mathematical knowledge management
Steven Kieffer, Jeremy Avigad, and Harvey Friedman.
Studies in Logic, Grammar and Rhetoric (special issue on computer reconstruction of the body of mathematics), 18:51-66, 2009.
Paper: journal, arXiv, associated materials: html.The metamathematics of ergodic theory
Jeremy Avigad.
Annals of Pure and Applied Logic, 157:64-76, 2009.
Paper: doi, preprint: pdf.Functional interpretation and inductive definitions
Jeremy Avigad and Henry Towsner.
Journal of Symbolic Logic, 74:1100-1120, 2009.
Paper: doi, preprint: arXiv.Local stability of ergodic averages
Jeremy Avigad, Philipp Gerhardy, and Henry Towsner.
Transactions of the American Mathematical Society, 362:261-288, 2010.
Paper: doi, pdf, preprint: arXiv.Response to questionnaire
Jeremy Avigad.
In Vincent F. Hendricks and Hannes Leitgeb, editors, Philosophy of Mathematics: 5 questions, Automatic / VIP Press, 2007.
Book site: html, preprint: pdf.A decision procedure for linear "big O" equations
Jeremy Avigad and Kevin Donnelly. Journal of Automated Reasoning 38: 353-373, 2007.
Paper: doi, preprint: arXiv, implementation: sml.A variant of the double-negation translation
Jeremy Avigad.
Carnegie Mellon Technical Report CMU-PHIL 179.
Paper: pdfGödel and the metamathematical tradition
Jeremy Avigad.
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.Computers in mathematical inquiry
Jeremy Avigad.
In Paolo Mancosu, editor, The Philosophy of Mathematical Practice, Oxford University Press, 302-316, 2008.
Reprint: pdf, preprint: pdf.Understanding proofs
Jeremy Avigad.
In Paolo Mancosu, editor, The Philosophy of Mathematical Practice, Oxford University Press, 317-353, 2008.
Reprint: pdf, preprint: pdf.Combining decision procedures for the reals
Jeremy Avigad and Harvey Friedman.
Logical Methods in Computer Science, 2(4:4):1-42, 2006.
Paper: doi, arXiv
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, reprint: pdf, preprint: arXiv, project page and proof scripts: html.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
Methodology and metaphysics in the development of Dedekind's theory of ideals
Jeremy Avigad.
In José Ferreirós and Jeremy Gray, editors, The Architecture of Modern Mathematics, Oxford University Press, 159-186, 2006.
Uncorrected proofs: pdf, preprint: pdf.Notes on a formalization of the prime number theorem
Jeremy Avigad.
Carnegie Mellon Technical Report CMU-PHIL-163, 2004.
Paper: pdf.Philosophy of mathematics
Jeremy Avigad.
In Constantin Boundas, editor, The Edinburgh Companion to Twentieth-Century Philosophies, Edinburgh University Press, 234-251, 2007, also published as The Columbia Companion to Twentieth-Century Philosophies, Columbia University Press, 2007.
Preprint: pdf.Dedekind's 1871 version of ideal theory
Jeremy Avigad.
Translation, with an introduction; Carnegie Mellon Technical Report CMU-PHIL-162, 2004.
Paper: pdf, the original: pdf.Mathematical method and proof
Jeremy Avigad.
Synthese 153:105-159, 2006.
Paper: doi, preprint: pdf.Formalizing O notation in Isabelle/HOL
Jeremy Avigad and Kevin Donnelly.
In David Basin and Michaël Rusinowitch, editors, Automated Reasoning: second international joint conference, IJCAR 2004, Lecture Notes in Artificial Intelligence 3097, Springer, 357-371, 2004.
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.Forcing in proof theory
Jeremy Avigad.
Bulletin of Symbolic Logic, 10:305-333, 2004. (Awarded a 25th Anniversary Prize by the Bulletin.)
Paper: doi, jstor, bsl. Preprint: pdf. Erratum: html.Eliminating definitions and Skolem functions in first-order logic
Jeremy Avigad.
ACM Transactions on Computational Logic, 4:402-415, 2003. (Conference version: Logic in Computer Science 2001, Springer, 139-146.)
Paper: doi, reprint: pdf, preprint: pdf.Weak theories of nonstandard arithmetic and analysis
Jeremy Avigad.
In Stephen Simpson, editor, Reverse Mathematics 2001, A K Peters, 19-46, 2005.
Preprint: pdf.Notes on Pi^1_1 conservativity, omega-submodels, and the collection schema
Jeremy Avigad.
Carnegie Mellon Technical Report CMU-PHIL-125, 2001.
Paper: pdf.Number theory and elementary arithmetic
Jeremy Avigad.
Philosophia Mathematica, 11:257-284, 2003.
Paper: doi, preprint: pdf.Saturated models of universal theories
Jeremy Avigad.
Annals of Pure and Applied Logic, 118:219-234, 2002.
Paper: doi, preprint: pdf.Algebraic proofs of cut elimination
Jeremy Avigad.
Journal of Logic and Algebraic Programming, 49:15-30, 2001.
Paper: doi, preprint: pdf.Update procedures and the 1-consistency of arithmetic
Jeremy Avigad.
Mathematical Logic Quarterly, 48:3-13, 2002.
Paper: 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.An ordinal analysis of admissible set theory using recursion on ordinal notations
Jeremy Avigad.
Journal of Mathematical Logic, 2:91-112, 2002.
Paper: doi, preprint: pdfTransfer principles in nonstandard intuitionistic arithmetic
Jeremy Avigad and Jeffrey Helzner.
Archive for Mathematical Logic, 41:581-602, 2002.
Paper: doi, preprint: pdf.Ordinal analysis without proofs
Jeremy Avigad.
In W. Sieg et al. eds., Reflections on the Foundations of Mathematics: Essays in Honor of Solomon Feferman, ASL Publications, A K Peters, 1-36, 2002.
Preprint: pdf.Interpreting classical theories in constructive ones
Jeremy Avigad.
Journal of Symbolic Logic, 65:1785-1812, 2000.
Paper: jstor, euclid, preprint: pdf.A realizability interpretation for classical arithmetic
Jeremy Avigad.
In Buss, Hájek, and Pudlák eds., Logic Colloquium '98, AK Peters, 57-90, 2000.
Preprint: pdfThe model-theoretic ordinal analysis of predicative theories
Jeremy Avigad and Richard Sommer.
Journal of Symbolic Logic, 64:327-349, 1999.
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
Jeremy Avigad.
In Beame and Buss eds., Proof Complexity and Feasible Arithmetics, American Mathematical Society, 1-12, 1997.
Preprint: pdf.A model-theoretic approach to ordinal analysis
Jeremy Avigad and Richard Sommer.
Bulletin of Symbolic Logic, 3:17-52, 1997.
Paper: jstor, euclid,bsl, preprint: pdf. An effective proof that open sets are Ramsey
Jeremy Avigad.
Archive for Mathematical Logic, 37:235-240, 1998.
Paper: doi, preprint: pdf.Predicative functionals and an interpretation of ID^_<omega
Jeremy Avigad.
Annals of Pure and Applied Logic, 92:1-34, 1998.
Paper: doi, preprint: pdf.Formalizing forcing arguments in subsystems of second-order arithmetic
Jeremy Avigad.
Annals of Pure and Applied Logic, 82:165-191, 1996.
Paper: doi, preprint: pdf.On the relationship between ID^_<omega and ATR_0
Jeremy Avigad.
Journal of Symbolic Logic, 61:768-779, 1996.
Paper: jstor, euclid, preprint: pdf.