I am a mathematical logician and philosopher of mathematics, working
in the tradition of David Hilbert's *Beweistheorie,* or "proof
theory." I am specifically interested in applying proof-theoretic methods in
mathematics, computer science, and philosophy.

The work described below represents a range of interests, but is generally based on a resolutely syntactic approach to making sense of mathematical method and proof. The list of publications is not exhaustive; for a complete list, see either my CV or Publications and Reviews. Slide presentations of some of this material can be found under Talks.

My current research interests and projects can be summarized as follows:

*Mathematical*

I am interested in "proof mining," that is, using proof-theoretic methods to obtain useful combinatorial, computational, and quantitative information from nonconstructive mathematical arguments. I am generally interested in computational and quantitative aspects of ergodic theory and dynamical systems, and other branches of analysis.*Computational*

I am interested in using formal methods towards verifying mathematical proofs and calculations, and to support mathematical reasoning. I am contributing to the development of a new theorem prover,*Lean*. The project page is here.*Philosophical*

I am interested in using historical and logical insights towards getting a better philosophical grasp of the notion of mathematical understanding.

Some my work to date is described in the sections that follow.

A good deal of twentieth-century work in proof theory involved finding formal "reductions" of one axiomatic theory to another, showing how, for example, infinitary or nonconstructive axioms can be interpreted in finitary or computational terms. To that end, I have used and extended many of the standard tools, including cut elimination, normalization, realizability and functional interpretation, semantic interpretations, double-negation translations, ordinal analysis, and forcing arguments. See, for example:

Proof theory

*Introduction to Formal Philosophy*, edited by Vincent F. Hendricks and Sven Ove Hansson, to appear. Draft: pdf.Functional interpretation and inductive definitions

with Henry Towsner,*Journal of Symbolic Logic*, 74:1100-1120, 2009. Paper: doi. 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.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.Number theory and elementary arithmetic

*Philosophia Mathematica,*11:257-284, 2003. Paper: doi. Reprint: pdf.Interpreting classical theories in constructive ones

*Journal of Symbolic Logic,*65:1785-1812, 2000. 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.

Update procedures and the 1-consistency of arithmetic

*Mathematical Logic Quarterly,*48:3-13, 2002. Paper: doi. Preprint: pdf.

The following papers can be seen as contributions to the field of reverse mathematics, where the goal is to calibrate the axiomatic strength required to carry out common mathematical arguments:

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.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.An effective proof that open sets are Ramsey

*Archive for Mathematical Logic,*37:235-240, 1998. Paper: doi. Preprint: pdf.

The reductions described in the previous section are reductions "in principle." For example, such a result may tell us that if a certain type of theorem can be proved in a formal axiomatic system, X, that has nonconstructive axioms, then it, or perhaps some related statement, can be proved in a corresponding constructive system, Y. But now suppose one has an ordinary mathematical theorem, proved using methods that are "nonconstructive" in the informal sense. Can proof-theoretic methods be used to provide any useful information?

Georg Kreisel proposed such a program of "unwinding" classical proofs in the 1950's and 1960's, but the idea has only recently begun to bear fruit. In particular, Ulrich Kohlenbach and his students have had impressive success in extracting useful results from nonconstructive proofs in functional analysis. Following a suggestion by Dana Scott, Kohlenbach has adopted the term "proof mining" to describe this type of research. Although it is somewhat dated, the following overview may be helpful:

Proof mining

A three-lecture tutorial. Slides: pdf.

I am particularly interested in understanding ergodic theory and dynamical systems in more explicit terms, including the applications of those theories to combinatorics and number theory. The following papers deal with this topic.

Ultraproducts and metastability

with José Iovino,*New York Journal of Mathematics*, 19:713-727, 2013. Journal: html.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.A metastable dominated convergence theorem

with Edward Dean and Jason Rute,*Journal of Logic and Analysis*, 4:3:1-19, 2012. Paper: doi.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.Metastability in the Furstenberg-Zimmer tower

with Henry Towsner,*Fundamenta Mathematicae*, 210:243-268, 2010. Paper: journal. Preprint: arXiv.The metamathematics of ergodic theory

*Annals of Pure and Applied Logic*, 157:64-76, 2009. Paper: doi. Preprint: pdf.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.

The following talks provide an overview of some of my interests in the area:

Computability and uniformity in ergodic theory

Slides: pdf.Computability, constructivity, and convergence in measure theory

Slides: pdf.

I am also interested in finding ways in which proof-theoretic insights can be used to support computational aspects of mathematics.

Since the early twentieth century, it has been commonly understood that ordinary mathematical arguments can be formalized in axiomatic theories like Zermelo-Fraenkel set theory. But once again, this was the case only "in principle"; even the most elementary mathematical arguments quickly grow unwieldy when reduced to axiomatic terms.

Within the last few decades, the advent of
computational proof assistants has made it possible to formalize
significant mathematical proofs *in practice*. Such proof
assistants provide supporting infrastructure, keeping track of axioms,
definitions, and theorems; carrying out calculations; and filling in
some of the details of a proof. One can find a survey of the field in the
December 2008 issue of the Notices of the AMS, as well as here:

Formally verified mathematics

with John Harrison,*Communications of the ACM*, 57(4):66-75, 2014. Paper: doi, author's link.

In the fall of 2004, with the help of some students at Carnegie Mellon, I completed a formally verified proof of the Hadamard / de la Vallée Poussin prime number theorem. The formalization is described here:

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.

The proof scripts are still available on an otherwise outdated web page.

I spent 2009-2010 academic year visiting the INRIA / Microsoft Research Joint Centre in Orsay, working on George Gonthier's project to verify the Feit-Thompson theorem. You can read about the end result here:

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.

Type inference in mathematics

*Bulletin of the European Association for Theoretical Computer Science*, 106:78-98, 2012. Paper: journal. Preprint: arXiv.

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.

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.

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.

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*, 1:34, 2017. Paper: doi.Theorem Proving in Lean

with Leonardo de Moura and Soonho Kong. Online: html, text: pdf.The Lean Reference Manual

with Leonardo de Moura, Gabriel Ebner, and Sebastian Ullrich. 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: pdfThe 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: html.

I am, more broadly, interested in seeing what a traditional, proof-theoretical understanding can contribute to interactive theorem proving. Here is some of the work I have done along these lines:

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.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.Combining decision procedures for the reals

with Harvey Friedman,*Logical Methods in Computer Science,*2(4:4):1-42, 2006. Paper: doi, arXiv

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

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.

The following papers develop a logical framework for verifying properties of systems that can be modeled with computable functions over the reals:

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.

Ed Dean, John Mumma, and I have undertaken a detailed analysis of
the use of diagrammatic reasoning in Euclid's *Elements*, which
can be used to support the formal verification of such proofs as
well:

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.

See also the papers "Mathematical method and proof," "Understanding proofs," and my review of Marcus Giaquinto's book on visualization and diagrammatic reasoning, discussed in the next section.

The philosophy of mathematics has long focused on questions as to the appropriate justification for mathematical knowledge, the sense in which mathematical statements are true, and the sense in which in which mathematical inferences are correct. But everyday mathematical discourse uses a much richer system of evaluatory assessments: theorems can be interesting, questions can be natural, definitions can be fruitful, concepts can be powerful, proofs can be elegant, and so on. A broader epistemology of mathematics should help clarify these value judgments as well.

I have made the case for such an expansion in a number of places; in addition to "Number theory and elementary arithmetic," listed above, see also: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.Review of Bonnie Gold and Roger A. Simons, *Proof and Other Dilemmas: Mathematics and Philosophy*

*Notices of the American Mathematical Society,*58(11): 1580-1584, 2011. Review: 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.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.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.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.Mathematical method and proof

*Synthese*153:105-159, 2006. Paper: doi. Preprint: pdf.

Some of the methodological and philosophical issues related to the study of visualization and diagrammatic reasoning in mathematics are discussed here:

Review of Marcus Giaquinto, *Visual Thinking in Mathematics: An Epistemological Study*

*Philosophia Mathematica,*17:95-108, 2009. Review: doi. Preprint: pdf.

The history of mathematics can provide valuable guidance towards uncovering what really matters to mathematics. Supported by an Andrew W. Mellon Foundation "New Directions" grant in 2003-2004, I was able to study seminal nineteenth century developments in mathematics. See, for example:

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.Dedekind's 1871 version of ideal theory

translation, with an introduction; Carnegie Mellon Technical Report CMU-PHIL-162, 2004. Paper: pdf. The original: pdf.

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.Character and object

with Rebecca Morris.*Review of Symbolic Logic*, 9:580-510, 2016. Published version: doi, pdf. Expanded version: pdf.

I am also interested in the history of logic, foundations, and the philosophy of mathematics.

Review of Eckart Menzler-Trott, *Logic's Lost Genius: The Life of Gerhard Gentzen*and Reinhard Kahle and Michael Rathjen, editors,*Gentzen's Centenary: The Quest for Consistency*

*Notices of the American Mathematical Society*, 63(11):1288-1292, 2016. Review: pdf.Review of S. Barry Cooper and Jan van Leeuwen, eds., *Alan Turing: His Work and Impact*

*Notices of the American Mathematical Society*, 61(8):886-890, 2014. Review: pdf.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.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.Review of William Tait, *The Provenance of Pure Reason: Essays in the Philosophy of Mathematics and its History*

*Bulletin of Symbolic Logic,*12:608-611, 2006. Review: bsl. Preprint: pdf.Review of Calixto Badesa, *The Birth of Model Theory: Löwenheim's Theorem in the Frame of the Theory of Relatives*

*The Mathematical Intelligencer,*28(4):67-71, 2006. Review: doi, Preprint: pdf.Review of Dennis E. Hesseling, *Gnomes in the Fog: The Reception of Brouwer's Intuitionism in the 1920s*

*The Mathematical Intelligencer,*28(4):71-74, 2006. Review: doi. Preprint: pdf."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.