Formalising the Top 100 Theorems using Isabelle
Originator and supervisor: Prof. Lawrence Paulson
There was an online list (archived here) of 100 well-known mathematical theorems, and a separate list indicating how many of these have been formalised in a variety of different interactive theorem provers. As of this writing, 46 of them had been formalised in Isabelle, the top system being HOL Light at 82.
The project is merely to identify and prove (using Isabelle) a selection of the not-yet-formalised theorems. The selection needs to be done with care, since typically a theorem is proved in the context of possibly a very substantial theory, which would also have to be developed by proof rather than assumed as a collection of axioms. It is also possible to include theorems that have been proved already, using a different proof. (Some theorems have several substantially different proofs.) It is acceptable to follow an existing HOL Light formalisation, but more interesting is to formalise a textbook development.
This project will suit students who have a mathematical background and who are already familiar with the theorems that they choose to formalise.