ERC logo

Project ID 742178

ALEXANDRIA: Large-Scale Formal Proof for the Working Mathematician

L. C. Paulson, Computer Laboratory, University of Cambridge

And the postdocs: Anthony Bordg, Angeliki Koutsoukou-Argyraki, Wenda Li, Yiannos Stathopoulos, and associated team members: Dr Sean Holden, Chelsea Edmonds, Albert (Qiaochu) Jiang, Chaitanya Mangla.

From the proposal

Mathematical proofs have always been prone to error. Today, proofs can be hundreds of pages long and combine results from many specialisms, making them almost impossible to check. One solution is to deploy modern verification technology. Interactive theorem provers have demonstrated their potential as vehicles for formalising mathematics through achievements such as the verification of the Kepler Conjecture. Proofs done using such tools reach a high standard of correctness.

However, existing theorem provers are unsuitable for mathematics. Their formal proofs are unreadable. They struggle to do simple tasks, such as evaluating limits. They lack much basic mathematics, and the material they do have is difficult to locate and apply.

ALEXANDRIA will create a proof development environment attractive to working mathematicians, utilising the best technology available across computer science. Its focus will be the management and use of large-scale mathematical knowledge, both theorems and algorithms. The project will employ mathematicians to investigate the formalisation of mathematics in practice. Our already substantial formalised libraries will serve as the starting point. They will be extended and annotated to support sophisticated searches. Techniques will be borrowed from machine learning, information retrieval and natural language processing. Algorithms will be treated similarly: ALEXANDRIA will help users find and invoke the proof methods and algorithms appropriate for the task.

ALEXANDRIA will provide (1) comprehensive formal mathematical libraries; (2) search within libraries, and the mining of libraries for proof patterns; (3) automated support for the construction of large formal proofs; (4) sound and practical computer algebra tools.

ALEXANDRIA will be based on legible structured proofs. Formal proofs should be not mere code, but a machine-checkable form of communication between mathematicians.

So what have we done?

I've written a survey of our formalisation work. Angeliki's Topos Institute talk "The Era of Formalised Mathematics" outlines the historical background as well as the project's achievements. The ERC website has the full list of publications. Some highlights:

We have formalised a wide selection of results across the mathematical landscape: combinatorics, analysis, number theory, Ramsey theory. We've formalised the work of two Fields medalists (Roth and Gowers) an Abel prize winner (Szemerédi) and the legendary Paul Erdős too. For background, commentary, examples, techniques and philosophical issues, see my Machine Logic blog!

The project ran for 72 months starting 1 September 2017.

Last revised: Wednesday, 7 February 2024

Lawrence C. PaulsonComputer LaboratoryUniversity of Cambridge