ACS Project Proposals by Prof L C Paulson
Each of these proposals 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.
Infinitesimal Geometry and Newton's Principia Mathematica
During the 1990s, Jacques Fleuriot used Isabelle to formalise some theorems from Isaac Newton's great volume, 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.
Bernstein Coefficients and Polynomials
Bernstein polynomials have many applications in mathematics and computer science. They underlie Bézier curves, and they can be used to isolate roots of polynomials and to estimate the maximum and minimum value reached by a polynomial. A number of other researchers have formalised this material; machine proofs in other systems (PVS and Coq) exist. There are three main propositions to prove in this theory. If time is available, applications could be developed.
A Library of Identities for Binomial Coefficients
The book Concrete Mathematics by Graham, Knuth and Patashnik includes 90 pages of material covering binomial coefficients and the dozens of beautiful identities that they satisfy. This material begins with laws that could be proved by induction and proceeds to increasingly advanced mathematical methods. This project provide experience with a variety of useful mathematical techniques, and the source material is very clear.
A Formalisation of Information Theory
Shannon's information theory is fundamental to many aspects of computer science, including cryptography, coding theory, data transmission and compression. It rests on an elaborate mathematical basis that includes integration theory, measure theory and probability theory. Most of this foundation has already been laid: a simple formalisation of information theory already exists in Isabelle. However, many of the fundamental theorems of information theory have yet to be formalised. A paper describing similar work conducted using the Coq system illustrates some of the tasks to be undertaken. Note that Coq proofs cannot easily be ported to Isabelle, because the logical formalisms are very different.
Formalising the Top 100 Theorems using Isabelle
There is an online list 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, 55 of them had been formalised in Isabelle, the top system being HOL Light at 86.
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.
It is equally acceptable to formalise interesting theorems not on that list, such as Goodstein's theorem.