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..
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.
For my dissertation, I have implemented a proof-producing version of my masters project within 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 on Jasmin Blanchette's Matryoshka project.
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.
A bi-directional extensible ad hoc interface between Lean and Mathematica (with Minchao Wu)
An extensible ad hoc interface between Lean and Mathematica
A heuristic prover for real inequalities (journal version)(with Jeremy Avigad and Cody Roux)
Journal of Automated Reasoning, 2016
A heuristic prover for real inequalities (conference version)(with Jeremy Avigad and Cody Roux)
Energy minimizing unit vector fields (with Leobardo Rosales, et al)
Involve 3(4), 2010