I am Professor of Computational Logic at the Computer Laboratory, University of Cambridge, UK. My research concerns automated theorem proving and its applications. I originated and continue to develop the interactive theorem prover Isabelle. I also built MetiTarski, an automatic prover for the elementary functions.

Using Isabelle, I have formalized deep results of set theory: the reflection theorem and the relative consistency of the axiom of choice. I have recently completed the first machine-assisted formalisation of Gödel's second incompleteness theorem. This extends the first incompleteness theorem to state that any suitable formal system that can prove its own consistency is in fact inconsistent.

One of my current research objectives is to unite MetiTarski and Isabelle by formalising in the latter the mathematical facts assumed by the former.

I have a B.S. degree from Caltech in mathematics (covering chiefly logic, but also analysis and combinatorics). My PhD (from Stanford) is in computer science.