Welcome

Research

Papers

Books

Reviews

Talks

Teaching

Students

Research

I am a mathematical logician and philosopher of mathematics who uses logical methods to understand mathematical language, mathematical proof, and the principles of mathematical reasoning. I have been interested in applying these methods in mathematics, computer science, and philosophy. Currently, my primary research interests are in formal methods and AI for mathematics.

Mathematical Logic

I was trained in the tradition of David Hilbert's Beweistheorie, or proof theory, which involves modeling mathematical reasoning in formal axiomatic systems and studying those systems in syntactic terms. My book, Mathematical Logic and Computation, tries to preserve the elements of that tradition that are still relevant to mathematics, computer science, and philosophy today.

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. For an overview, see here: To that end, I have used and extended many of the standard tools, including cut elimination, normalization, realizability, functional interpretation, semantic interpretations, double-negation translations, ordinal analysis, and forcing arguments. See, for example: 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:

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:

Ed Dean, John Mumma, and I have undertaken a detailed analysis of the use of diagrammatic reasoning in Euclid's Elements.

Applications of Logic to Mathematics

I have been interested in the way that logical methods can expose quantitative or computational information that is implicit in classical mathematics, in fields such as ergodic theory and dynamical systems.

The following talks provide an overview of some of that work:

Formalization of Mathematics

Computational proof assistants now make it possible to represent mathematical definitions and theorems in digital formats that can be processed and checked mechanically. The following provide general information about the field.

I have been working in the field since the early 2000s. In the fall of 2004, with some students at Carnegie Mellon, I completed a formally verified proof of the Hadamard / de la Vallée Poussin prime number theorem.

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.

I did some early work in homotopy type theory and verified the central limit theorem with Johannes Hölzl and Luke Serafin. I have been contributing to the development of the Lean Theorem Prover since its inception. I led the development of the first libraries and documentation, and I am proud to say that a large number of my students, postdocs, and visitors have worked on it over the years. (See the fifth slide of this talk.) See also the tutorials and documentation listed under Books, the courses and materials listed under Teaching and the Lean community web pages. Since 2021, I have been the director of the Hoskinson Center for Formal Mathematics, and our current work is described on the web pages.

I am interested in applications of formal methods to applied mathematics as well.

Formal Verification and Automated Reasoning

I am interested in automated reasoning for mathematics and formal verification.

I am working with students and colleagues on automated reasoning for Lean.

Since 2021, I have served as a consultant for StarkWare, verifying their language and library for blockchain applications.

The following papers develop a logical framework for verifying properties of systems that can be modeled with computable functions over the reals. The associated tool, dReal, is maintained by Soonho Kong and actively used at Amazon Web Services.

AI for Mathematics

I am currently exploring applications of neural AI and machine learning to mathematics, chiefly in combination with symbolic methods. In addition to the paper on premise selection listed in the previous section, these fall under that category: The following essay emphasizes the importance of symbolic methods in AI: The following talks emphasize important priorities in the development of AI for mathematics:

Philosophy of Mathematics

I have long been interested in making sense of mathematical understanding, paying close attention to mathematical language.

This talk provides a survey overview of some of the ways I think about mathematical understanding:

History of Mathematics

Studying the history of mathematics and seeing how it has evolved provides valuable insights into what drives the subject and how it works. I have studied nineteenth century mathematics with that aim in mind.

I have also taught graduate and undergraduate seminars on the history of mathematics; see Teaching.

History of Logic

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