I'm interested in automated reasoning and formalizing mathematics.

Imogen

Imogen is the name of what will be a series of theorem provers for nonclassical logics using the focused inverse method. The first variant of Imogen, the case of intuitionistic propositional logic, was recently completed. You can read a preprint, or download Imogen.

Flyspeck

The Flyspeck project seeks to formalize Thomas Hales' 1998 proof of the Kepler Conjecture in the interactive theorem prover HOL Light.

Kepler Code

As a step toward Flyspeck, I am rewriting all of Hales' original C++, Java, and Mathematica code in Standard ML. There are a number of reasons for this. Standard ML is much closer to the functional languages found in modern theorem provers. Hales code was also written over a period of 10 years, in a number of different languages and with the help of his students. I want the verifications that are carried out by computer to be easy to reproduce in ML, and thus easier to port to a theorem prover.

Logosphere

Logosphere is a database of proofs.

The Dodecahedral Conjecture