ACS Project Proposals by Prof L C Paulson
Each of the proposals below involves formalising mathematics using the proof assistant Isabelle/HOL. Such projects will suit students who have a mathematical background, especially if they are already familiar with the theorems that they choose to formalise.
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, 83 of them had been formalised in Isabelle, the top system being HOL Light at 86. It looks like all the reasonably straightforward theorems have been taken. Fortunately, there are many other theorems of interest.
Real Root Isolation
This a project to build an efficient real root isolation procedure based on Descartes’ rule of signs, following this paper. The ultimate goal might be to formalise the state-of-the-art version, but that's probably too much; it's possible to omit advanced features like partial Taylor shift and approximate arithmetic. The starting point of this project is rather moderate: to certify the termination of the procedure. This requires the theorem of three circles, which is already available in another proof assistant, Coq.Stirling Number Identities
A paper entitled Close Encounters with the Stirling numbers of the Second Kind treats a variety of identities connected with binomial coefficients and Stirling numbers. These identities do not appear to have elementary proofs by induction. They must instead be proved using the technique of generating functions, or possibly, by combinatorial arguments: by comparing the cardinalities of finite sets satisfying certain criteria. Neither approach is straightforward. The student should study this paper before committing to the project; prior familiarity with generating functions is advisable.
The Four Colour Map Theorem
This celebrated theorem was first proved in 1976 with the help of a computer program to check nearly 2000 cases. Mathematicians did not like the idea of a proof checked by code, but Georges Gonthier's 2008 formalisation using the Coq proof assistant definitively established the result. The proof still involved a computer program checking numerous cases, but the program had been generated and proved to be correct within Coq itself.
The four colour proof is too big to be tackled as a single ACS project, but Gonthier has helpfully broken it down into modules, any one of which would be suitable:
- The theory of planar hypermaps, up to the combinatorial Jordan Curve theorem (both ways), configuration cut-and-paste, and maybe configuration isomorphism. (This foundational material is also relevant to the Flyspeck Project.)
- The reducibility procedure, verified against an abstract notion of reducibility (plus possibly unverified colouring generation).
- The reduction to a combinatorial problem, which involves some real topology.
Gonthier's full report on his work explains the necessary mathematics.
Infinitesimal Geometry and Newton's Principia Mathematica
During the 1990s, Jacques Fleuriot used Isabelle to formalise some theorems from Isaac Newton's Philosophiæ Naturalis Principia Mathematica, which developed the mathematical theory of gravity and the orbits of the planets. Where Newton used geometrical arguments involving infinitesimals and other unusual methods, Fleuriot used an axiomatic system for geometry coupled with a formalisation of non-standard analysis. His Ph.D. research gave a rigorous basis to Newton's apparently imprecise use of infinitesimal reasoning, and won a national award. He even found an error in one of Newton's proofs.
The proposal is to redo some of this work using Isabelle as it is now and using a neater axiomatic basis for geometry, proposed by Fleuriot himself. The project will be an unusual combination of interactive theorem proving and the history of science. Isabelle's existing formalisation of non-standard analysis will be used, so the project will be concerned with formalising geometric concepts and applying them to some of Newton's proofs, starting with those treated by Fleuriot.
Last revised: Friday, 18 September 2020