Welcome

Research

Papers

Books

Reviews

Talks

Teaching

Students

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: pdf
• Gö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: pdf
• Transfer 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: pdf
• The 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.