BP.IO / POST

Isabelle Theorem Proving

From November 2005 to February 2006 I worked with the University of New South Wales, and National ICT Australia on a project entitled Top 100 Theorems. The project involved formalising some mathematical theorems into the Isabelle proof checker. A Top 100 list of popular mathematical theorems and the progress people have made in formalising them is on the web.