Research

My research interests fall broadly into the category of formal methods, more specifically in interactive theorem proving and automated reasoning. Disciplinary questions are difficult; I consider myself a logician, a theoretical computer scientist, or an applied mathematician, depending on the day. I publish primarily in computer science.

See my CV for a list of my publications, presentations, and drafts.

Summary

Proof assistants are tools that provide languages for defining objects, stating properties of these objects, and proving that these properties hold; they also offer engines for verifying the correctness of these proofs. Automated reasoning tools, including SAT solvers, SMT solvers, and first- and higher-order provers, are by contrast push-button tools that check the correctness of a statement. While they are sometimes used in the context of a proof assistant to close proof obligations automatically, they are seen more often in unverified settings.

My goal as a researcher is to adapt the logics, tools, and paradigms of formal methods in computer science to attack mathematical problems. I envision a future where trustworthy computer assistance in mathematical research is commonplace. The routine use of proof assistants will increase the reliability of proofs; large libraries of formal proofs will be used for reference and training by students and AI programs; advances in automated reasoning will do away with tedious parts of proving.

Projects

Early in the course of my PhD studies, I became one of the first users of Lean, a proof assistant based on dependent type theory. I am an active contributor to and maintainer of the Lean standard library, an open-source community effort that serves as a base for much of my work.

I have recently worked on a number of mathematical formalizations in Lean, as part of the Lean Forward project.

As part of my dissertation, I developed a method for automatically proving nonlinear inequalities. Extensions of this tool remain in active development. The system Draws on theory combination methods like SMT, to combine separate solvers for linear arithmetic, multiplicative arithmetic, and other theories in a heuristic proof search.

Another project of mine integrates Lean with the computer algebra system (CAS) Mathematica. The link I have developed is generic, extensible, and can be used for communication in both directions.

To spread formal methods more widely, mathematicians and computer scientists must collaborate. Pushing this collaboration is an essential part of my research project. I have organized interdisciplinary workshops working toward this goal.

I am very interested in the use of proof assistants in mathematics and computer science education. Jeremy Avigad, Floris van Doorn, and I have developed a mathematical reasoning textbook that incorporates Lean.

My general interests also include the philosophical and psychological aspects of mathematical reasoning. While my published work is largely technical, I am curious about how developments in formal languages and automated proof can shed light on traditional mathematical practice.

Slides

Here is an assortment of slides from some talks I’ve given:

• Formalizing the ring of Witt vectors (video)
• Simplifying casts and coercions
• The Lean mathematical library (video)
• Formalizing the solution to the cap set problem
• Formalized mathematics in Lean
• A formal proof of Hensel’s lemma over the p-adic integers
• A heuristic method for formally verifying real inequalities
• Toward AI for Lean, via metaprogramming
• The Lean theorem prover, for mathematicians
• An extensible ad-hoc interface between Lean and Mathematica
• Automation and computation in the Lean theorem prover
• Dependent types and the algebraic hierarchy
• Dissertation defense
• MS thesis defense