Research
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 logical methods to
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 research has generally fallen into three categories:
- Mathematical
I am interested in the way that mathematics balances the need for abstract, conceptual understanding on the one hand and pragmatic computation on the other. I have used logical methods to locate combinatorial, computational, and quantitative information that is implicit in proofs in fields like ergodic theory and dynamical systems.
- Computational
I am interested in the way that formal methods from computer science can be used to support mathematical reasoning. I have contributed to the development of a proof assistant, Lean, and its libraries. (The project page is here and the Lean community web pages are here.)
- Philosophical
I am interested in using historical and logical insights to get a better philosophical grasp of mathematics and mathematical understanding.
Some my work to date is described in the sections that follow. These days, I spend most of my time on the second of these categories.
Metamathematics and proof theory
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.
One of my favorite results is something of a curiosity, namely, a
characterization of classical propositional logic using one
connective, one axiom, and one rule:
- Plausibly hard combinatorial tautologies
in
Beame and Buss eds., Proof Complexity and Feasible
Arithmetics, American Mathematical Society, 1-12, 1997.
Preprint: pdf.
Many years ago (initially with Rick Sommer), I worked on developing
a more semantic, combinatorial approach to ordinal analysis. This did
not work out as well as I would have liked, but I am still fond of the
following approach the ordinal analysis of classical
first-order arithmetic:
- 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.
Proof mining and computational mathematics
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.
Formal verification and automated reasoning
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:
- The mechanization of mathematics
Notices of the AMS, 65(06):681-690, 2018. Paper: doi.
- Formally verified mathematics
with John Harrison, Communications of the ACM, 57(4):66-75, 2014. Paper: doi, pdf.
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.
The following describes some the mechanisms that are used in the project to
model ordinary algebraic reasoning:
- Type inference in mathematics
Bulletin of the European Association for Theoretical Computer
Science, 106:78-98, 2012. Paper: journal.
Preprint: arXiv.
The following is a contribution to homotopy type theory:
- 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.
More recently, I verified the Central Limit Theorem with Johannes Hölzl and Luke Serafin:
- 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.
I am also interested in developing tools to provide better support for interactive theorem proving:
- 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.
I am currently contributing to the development of a new theorem prover, Lean.
- The Lean mathematical library
by The mathlib Community. Certified Proofs and Programs (CPP) 2020. Paper: doi, project page: html, repository: github.
- 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: pdf
- An Introduction to Lean
with Gabriel Ebner and Sebastian Ullrich. Online: html, text: 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: html.
Floris van Doorn, Robert Lewis, and I are developing an undergraduate introduction to logic and proof, which incorprates exercises based on Lean:
- Logic and Proof
with Floris van Doorn and Robert Lewis. Online: pdf, text: pdf
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: doi, 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.
Philosophy and history of mathematics
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:
- The design of mathematical language
Draft: philsci archive.
- Reliability of mathematical inference
To appear in Synthese. Paper: doi, preprint: philsci archive.
- Principia
An article in Aeon magazine: html
- Modularity in mathematics
Review of Symbolic Logic, 13:47-79, 2020.
Preprint: doi, philsci archive.
- 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.
Rebecca Morris and I have written two papers on the history Dirichlet's theorem on primes in an arithmetic progression, and what that history has to tell us about the methods of mathematics:
- 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:480-510, 2016.
Published version: doi, pdf.
Expanded version: pdf.
The first adopts a more mathematical and historical perspective, while the second focuses on how these history informs the philosophy of mathematics, and our understanding of Frege's work in the foundations of mathematics. See also the following talks: pdf,
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.