ACS Project Proposal by Prof L C Paulson
The proposal is to formalise a piece mathematics using the proof assistant Isabelle/HOL. More than one student can undertake such a project. They are ideal if you have a mathematical background, especially if you are already familiar with the theorems that you choose to formalise. Specific suggestions will be added below, and your own choices should also be possible provided the level of difficulty is appropriate.
There is an online list of 100 well-known mathematical theorems, and a separate list indicating how many of these have been formalised in various proof assistants. As of this writing, 89 of them had been formalised in Isabelle, just above HOL Light at 87. Every theorem on the list has been formalised using one system or another, except for one: Fermat's last theorem!
Numerous students have undertaken this project in the past, through summer internships, the MPhil, Part III and occasionally, Part II. In many cases, their work has been published on Isabelle's Archive of Formal Proofs, where it lives forever. Examples include Turán's Graph Theorem, the Polygonal Number Theorem, Kneser's Theorem and the Balog–Szemerédi–Gowers Theorem.
Last revised: Monday, 25 September 2023