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.

Theorem Proving in Lean

with Leonardo de Moura and Soonho Kong. Online: html, text: pdf.Programming in Lean

with Leonardo de Moura and Jared Roesch. Online: html, text: pdfAn Introduction to Lean

with Gabriel Ebner and Sebastian Ullrich. Online: html, text: pdfLogic and Proof

with Floris van Doorn and Robert Lewis. Online: html, text: pdf

A metaprogramming framework for formal verification

Gabriel Ebner, Sebastian Ullrich, Jared Roesch, Jeremy Avigad, Leonardo de Moura. To appear in*International Conference on Functional Programming 2017*.Modularity in mathematics

Draft: pdf.A formally verified proof of the Central Limit Theorem

with Johannes Hölzl and Luke Serafin. To appear in the*Journal of Automated Reasoning*, 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:580-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, author's link.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, 2104. 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

Invited chapter for Sven Ove Hansson and Vincent F. Hendricks, editors,*Handbook of Formal Epistemology*, to be published by Springer. 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: 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: pdfGö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. 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: pdfTransfer 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: pdfThe 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.