I work at the intersection of mathematics and computer science, focusing on the fields of automated mathematical reasoning and interactive theorem proving.

For my masters project, I developed (with Jeremy Avigad and Cody Roux) a heuristic procedure for reasoning with real-valued inequalities. The procedure works on extensions of the language of real closed fields including multiplication by rational constants and uninterpreted functions with axiomatic constraints. I presented the project at ITP in July 2014.

The source code for our project, and brief instructions to run it, is available on Github. Our paper in ITP (see below) describes the project in some detail; my MS thesis goes into much more detail. You can also see the slides for my thesis defense.

I am helping develop the standard library for the Lean theorem prover, currently under development at Microsoft Research. Lean is a system similar to Coq, based on dependent type theory. It aims to bridge the gap between automated and interactive verification in mathematics and computer science. My contributions include parts of the algebraic hierarchy, the construction of the reals, the Frechet derivative and other components of the analysis theory, and some linear algebra. I am working toward verifying some results concerning sphere packings.

I am working toward implementing a proof-producing version of my masters project within Lean. This development will include tools for automated linear arithmetic. I have also implemented an ad-hoc connection between Lean and Mathematica, allowing the import and verification of computer algebra results.

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.

See my CV for a concise, up-to-date list of publications and presentations.

### Publications

A heuristic prover for real inequalities (with Jeremy Avigad and Cody Roux)

Journal of Automated Reasoning, 2016

Abstract

We describe a general method for verifying inequalities between realvalued expressions, especially the kinds of straightforward inferences that arise in interactive theorem proving. In contrast to approaches that aim to be complete with respect to a particular language or class of formulas, our method establishes claims that require heterogeneous forms of reasoning, relying on a Nelson-Oppen style architecture in which special-purpose modules collaborate and share information. The framework is thus modular and extensible. A prototype implementation shows that the method works well on a variety of examples, and complements techniques that are used by contemporary interactive provers.

Energy minimizing unit vector fields (with Leobardo Rosales, et al)

Involve 3(4), 2010

Abstract

Given a surface of revolution with boundary, we study the extrinsic energy of smooth tangent unit-length vector fields. Fixing continuous tangent unit length vector fields on the boundary of the surface of revolution, we ask if there is a unique smooth tangent unit-length vector field continuously achieving the boundary data and minimizing energy amongst all smooth tangent unit-length vector fields also continuously achieving the boundary data.

### Talks

Automation and Computation in the Lean Theorem Prover

AITP: Artificial Intelligence in Theorem Proving. April 2016

TU Munich Logic and Verification seminar. March 2016

Abstract

Lean is a new proof environment being developed at Microsoft Research. Based on dependent type theory, Lean combines an efficient elaboration process with a powerful type class inference mechanism. We describe how these features have been used in the development of the standard library, and why they make Lean a good environment for general automated methods. Ultimately, Lean aims to bridge the gap between user-centric interactive theorem proving and machine-centric automated theorem proving. We also outline a novel automated procedure for proving inequalities over the real numbers that is currently being implemented.

Algebra and Analysis in the Lean Theorem Prover

MAP 2016: Effective Analysis. January 2016

Abstract

Lean is a new proof assistant based on dependent type theory, being developed at Microsoft Research and CMU. A powerful and efficient type class mechanism allows us to construct and reason about the algebraic hierarchy and concrete number systems in a uniform, robust way. In this talk, I will explain the implementation of algebraic structures and the real numbers in Lean, and why this approach eases the development of further automation. I will also describe Polya, an automated tool for verifying real-valued inequalities which is being implemented in Lean.

Dependent types and the algebraic hierarchy

CARMA Workshop on Mathematics and Computation. Newcastle, NSW, Australia. June 2015

Abstract

A proof assistant for mathematics should recognize relationships been algebraic structures and instances; for example, that every semigroup is a group, a ring extends both an additive group and a multiplicative monoid, and the integers are an instance of an ordered ring. Managing these relationships makes it possible to use definitions, theorems, and notation developed for semigroups, for example, when reasoning about arbitrary rings, and the integers in particular.

We describe a way of accomplishing this, implemented in the Lean theorem prover. Lean is based on dependent type theory, and expressive foundational language in which every object has an associated "type". Lean supports a mechanism known as type class inference, which was originally designed to support generic programming in functional programming languages. I will explain how dependent type theory and type classes are ideally suited to managing the algebraic hierarchy as well.

A heuristic prover for real inequalities

Interactive Theorem Proving. Vienna, Austria. July 2014

6th Podlasie Conference on Mathematics. Bialystok, Poland. July 2014

Abstract

We describe a general method for verifying inequalities between realvalued expressions, especially the kinds of straightforward inferences that arise in interactive theorem proving. In contrast to approaches that aim to be complete with respect to a particular language or class of formulas, our method establishes claims that require heterogeneous forms of reasoning, relying on a Nelson-Oppen style architecture in which special-purpose modules collaborate and share information. The framework is thus modular and extensible. A prototype implementation shows that the method works well on a variety of examples, and complements techniques that are used by contemporary interactive provers.

Computers in mathematics: automated and interactive proofs

CMU Summer School in Logic and Formal Epistemology. Pittsburgh, PA. June 2014

Slides