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.