Research

I am a mathematical logician and philosopher of mathematics, working in the tradition of David Hilbert's "Beweistheorie," or "proof theory." From that perspective, mathematics is a fundamentally linguistic activity, governed by norms and conventions that can be studied in syntactic terms. 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. Summaries of many of the findings and results discussed here can be found under Talks.

Current interests

My current research interests 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. In particular, I am interested in computational and quantitative aspects of ergodic theory and dynamical systems, and aspects of algorithmic randomness.

Computational: I am interested in formal verification, and, specifically, verifying mathematical proofs and mathematical computation. I am working with Chris Kapulkin on deriving properties of fibration categories in homotopy type theory, and with Ed Clarke and Sean (Sicun) Gao on numerical methods of verifying the safety of hybrid systems. I am also interested in developing better automated support for verifying mathematics.

Philosophical: I am interested in using historical and logical insights towards getting a better philosophical grasp of the notion of mathematical understanding. I am working with Rebecca Morris to study methodological aspects of the development of mathematics in the nineteenth century, and I will be teaching a seminar on mathematical understanding in the fall of 2012.

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

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:

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: 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:

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:

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 some 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:

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.

The following talk provides an overview of some of my interests in the area:

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 current technology in the December 2008 issue of the Notices of the AMS.

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:

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 project here. The following describes some the mechanisms that are used in the project to model ordinary algebraic reasoning:

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:

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

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:

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 sixth of these is a survey of twentieth-century philosophy of mathematics; the first and fourth include more opinionated assessments of the philosophy of mathematics today. The other papers make the case that insights and issues that arise in formal verification are relevant to a broader and more robust epistemology of mathematics.

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

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:

I am also interested in the history of logic, foundations, and the philosophy of mathematics. Some personal reflections on that history can be found in the following: