Publications

This list includes research articles, surveys, expository articles, unpublished notes, and a translation. Many of these papers are also listed, arranged by subject matter, under Research. See also listings on MathSciNet, Zentralblatt, Google Scholar, DBLP, and Citeseer.

• ProofNet: A benchmark for autoformalizing and formally proving undergraduate-level mathematics problems
  with Zhangir Azerbayev and Bartosz Piotrowski (I am the third author), MATH-AI: Toward Human-Level Mathematical Reasoning, 2022. Paper: pdf
• Verified reductions for optimization
  with Alexander Bentkamp and Ramon Fernández (I am the third author). To appear in Tools and Algorithms for the Construction and Analysis of Systems (TACAS) 2023. Preprint: pdf.

• What we talk about when we talk about mathematics
  To appear in Karine Chemla, José Ferreirós, Lizhen Ji, Erhard Scholz, and Chang Wang, editors, The Richness of the History (and Philosophy) of Mathematics, to be published by Springer. Preprint: pdf. Notes on historical research: pdf.

• Two-sorted Frege arithmetic is not conservative
  with Stephen Mackereth (first author). To appear in the Review of Symbolic Logic. Preprint: doi.
• An impossible asylum
  with Seulkee Baek, Alexander Bentkamp, Marijn Heule, and Wojciech Nawrocki. To appear in the American Mathematical Monthly. Preprint: arXiv, doi.
• A verified algebraic representation of Cairo program execution
  with 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
  To appear in The Handbook of Philosophy of Mathematical Practice. Preprint: philsci archive.
• Verified optimization (work in progress)
  with Alexander Bentkamp (first author). Presented at Formal Methods for Mathematics 2021. Paper: pdf, arXiv.
• Varieties of mathematical understanding
  Bulletin of the American Mathematical Society, 59:99-117, 2022. Paper: doi.
• Foundations
  for the Handbook of Proof Assistants and their Applications in Mathematics and Computer Science, edited by Jasmin Blanchette and Assia Mahboubi, to published by Springer. Preprint: arXiv.

• Progress on a perimeter surveillance problem
  with Floris van Doorn. IEEE International Conference on Autonomous Systems (ICAS) 2021. Paper: pdf, preprint (longer version): arXiv.

• The Lean mathematical library
  by the mathlib Community, in Jasmin Blanchette and Cătălin Hritcu, editors, Certified Proofs and Programs (CPP) 2020, ACM Publications, 2020. Paper: doi, project page: html, repository: github.
• Reliability of mathematical inference
  Synthese, 198(8): 7377-7399, 2021. Paper: doi, preprint: philsci archive.
• Automated reasoning for the working mathematician
  Notes: pdf. Associated repository: github.
• A formalization of the mutilated chessboard theorem
  Notes: pdf.
• Quotients of polynomial functors
  with 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
  An article in Aeon magazine: html.
• Learning logic and proof with an interactive theorem prover
  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
  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
  with 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, Leonardo de Moura, Proceedings of the ACM on Programming Languages, International Conference on Functional Programming 2017, 1:34, 2017. Paper: doi.
• Modularity in mathematics
  Review of Symbolic Logic, 13:47-79, 2020. Preprint: doi, philsci archive.
• A formally verified proof of the Central Limit Theorem
  with 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
  with Leonardo de Moura, Soonho Kong, and Cody Roux. Unpublished: pdf.
• The Lean theorem prover (system description)
  with 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
  To appear 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
  with Rebecca Morris. Review of Symbolic Logic, 9:480-510, 2016. Published version: doi, pdf. Expanded version: pdf.
• A heuristic prover for real inequalities
  with 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. Here is a draft of a revised, expanded version: pdf.
• Formally verified mathematics
  with John Harrison, Communications of the ACM, 57(4):66-75, 2014. Paper: doi, pdf.
• A machine-checked proof of the Odd Order Theorem
  with Georges Gonthier (first author), Andrea Asperti, 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
  with Krzysztof Kapulkin and Peter LeFanu Lumsdaine. Mathematical Structures in Computer Science, 25:1040-1070, 2015. Paper: pdf. Print: arXiv. Formal proofs: github.
• Ultraproducts and metastability
  with José Iovino, New York Journal of Mathematics, 19:713-727, 2013. Journal: html.
• The concept of 'character' in Dirichlet's theorem on primes in an arithmetic progression
  with Rebecca Morris. Archive for History of Exact Sciences, 68:265-326, 2014. Paper: doi. Preprint: arXiv.
• Computability and analysis: the legacy of Alan Turing
  with 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
  with Jason Rute. Ergodic Theory and Dynamical Systems, 35(4):1009-1027, 2015. Preprint: arXiv. Journal: pdf.
• Uniform distribution and algorithmic randomness
  Journal of Symbolic Logic, 78:334-344, 2013. Paper: doi. Reprint: pdf. Preprint: arXiv.
• Delta-complete decision procedures for satisfiability over the reals
  with Sicun Gao (first author) 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
  with Sicun Gao (first author) and Edmund M. Clarke, in Logic in Computer Science (LICS), 315-324, 2012. Paper: doi. Preprint: arxiv.
• Type inference in mathematics
  Bulletin of the European Association for Theoretical Computer Science, 106:78-98, 2012. Paper: journal. Preprint: arXiv.
• A metastable dominated convergence theorem
  with 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
  with 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
  Notre Dame Journal of Formal Logic, 53:347-350, 2012. Paper: doi, Preprint: arXiv.
• Inverting the Furstenberg correspondence
  Discrete and Continuous Dynamical Systems, Series A, 32:3421-3431, 2012. Paper: doi. Preprint: arXiv.
• Zen and the art of formalization
  with Andrea Asperti, 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
  Introduction to Formal Philosophy, edited by Vincent F. Hendricks and Sven Ove Hansson, Springer, 177-190, 2018. Draft: 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.
• 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
  with Henry Towsner, Fundamenta Mathematicae, 210:243-268, 2010. Paper: journal. Preprint: arXiv.
• The computational content of classical arithmetic
  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
  with 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.
• A language for mathematical knowledge management
  with Steven Kieffer (first author) 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
  Annals of Pure and Applied Logic, 157:64-76, 2009. Paper: doi. Preprint: pdf.
• Functional interpretation and inductive definitions
  with Henry Towsner, Journal of Symbolic Logic, 74:1100-1120, 2009. Paper: doi. Preprint: arXiv.
• Local stability of ergodic averages
  with Philipp Gerhardy and Henry Towsner, Transactions of the American Mathematical Society, 362:261-288, 2010. Paper: doi, pdf. Preprint: arXiv.
• Response to questionnaire
  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
  with Kevin Donnelly, Journal of Automated Reasoning 38: 353-373, 2007. Paper: doi. Preprint: arXiv. Implementation: sml.
• A variant of the double-negation translation
  Carnegie Mellon Technical Report CMU-PHIL 179. Paper: 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.
• Computers in mathematical inquiry
  in Paolo Mancosu, editor, The Philosophy of Mathematical Practice, Oxford University Press, 302-316, 2008. Reprint: pdf. Preprint: pdf.
• Understanding proofs
  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
  with 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
  with 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
  with 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
  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
  Carnegie Mellon Technical Report CMU-PHIL-163, 2004. Paper: pdf.
• Philosophy of mathematics
  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
  translation, with an introduction; Carnegie Mellon Technical Report CMU-PHIL-162, 2004. Paper: pdf. The original: pdf.
• Mathematical method and proof
  Synthese 153:105-159, 2006. Paper: doi. Preprint: pdf.
• Formalizing O notation in Isabelle/HOL
  with 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
  with Ksenija Simic, Annals of Pure and Applied Logic, 139:138-184, 2006. Paper: doi. Preprint: pdf.
• Forcing in proof theory
  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
  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
  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
  Carnegie Mellon Technical Report CMU-PHIL-125, 2001. Paper: pdf.
• Number theory and elementary arithmetic
  Philosophia Mathematica, 11:257-284, 2003. Paper: doi. Reprint: pdf.
• Saturated models of universal theories
  Annals of Pure and Applied Logic, 118:219-234, 2002. Paper: doi. Preprint: pdf.
• Algebraic proofs of cut elimination
  Journal of Logic and Algebraic Programming, 49:15-30, 2001. Paper: doi. Preprint: pdf.
• Update procedures and the 1-consistency of arithmetic
  Mathematical Logic Quarterly, 48:3-13, 2002. Paper: doi. Preprint: pdf.
• The epsilon calculus
  with Richard Zach, in the Stanford Encyclopedia of Philosophy. Article: html.
• "Clarifying the nature of the infinite": the development of metamathematics and proof theory
  with 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
  Journal of Mathematical Logic, 2:91-112, 2002. Paper: doi. Preprint: pdf
• Transfer principles in nonstandard intuitionistic arithmetic
  with Jeffrey Helzner, Archive for Mathematical Logic, 41:581-602, 2002. Paper: doi. Preprint: pdf.
• Ordinal analysis without proofs
  in W. Sieg et al. eds., Reflections on the Foundations of Mathematics: Essays in Honor of Solomon Feferman, Lecture Notes in Logic 15, ASL Publications, A K Peters, 1-36, 2002. Preprint: pdf.
• Interpreting classical theories in constructive ones
  Journal of Symbolic Logic, 65:1785-1812, 2000. Paper: jstor, euclid. Preprint: pdf.
• A realizability interpretation for classical arithmetic
  in Buss, Hájek, and Pudlák eds., Logic Colloquium '98, Lecture Notes in Logic 13, AK Peters, 57-90, 2000. Preprint: pdf
• The model-theoretic ordinal analysis of predicative theories
  with Richard Sommer, Journal of Symbolic Logic, 64:327-349, 1999. Paper: jstor, euclid. Preprint: pdf.
• Gödel's functional ("Dialectica") interpretation
  with 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.
• A model-theoretic approach to ordinal analysis
  with Richard Sommer, Bulletin of Symbolic Logic, 3:17-52, 1997. Paper: jstor, euclid, bsl. Preprint: pdf.
• An effective proof that open sets are Ramsey
  Archive for Mathematical Logic, 37:235-240, 1998. Paper: doi. Preprint: pdf.
• Predicative functionals and an interpretation of ID^_<omega
  Annals of Pure and Applied Logic, 92:1-34, 1998. Paper: doi. Preprint: pdf.
• Formalizing forcing arguments in subsystems of second-order arithmetic
  Annals of Pure and Applied Logic, 82:165-191, 1996. Paper: doi. Preprint: pdf.
• On the relationship between ID^_<omega and ATR_0
  Journal of Symbolic Logic, 61:768-779, 1996. Paper: jstor, euclid. Preprint: pdf.