I work at the intersection of mathematics and computer science, focusing on the fields of automated mathematical reasoning and interactive theorem proving. See my CV for a list of my publications, presentations, and drafts.

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.

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

I am a contributor and maintainer of the standard library for the Lean theorem prover, currently under development at Microsoft Research.

In my dissertation, I describe a proof-producing version of my masters project implemented in Lean. This development includes 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.

I am now a postdoc at the Vrije Universiteit Amsterdam on Jasmin Blanchette’s Matryoshka project. I am a collaborator on Blanchette’s Lean Forward project and Thomas Hales’ Formal Abstracts project.

I am very interested in the use of proof assistants in mathematics 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 are an assortment of slides from some talks I’ve given:

- 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