The ALEXANDRIA Project: what has been accomplished?
[general ALEXANDRIA Isabelle Archive of Formal Proofs HOL Light Principia Mathematica One of the my first posts described ALEXANDRIA, my ERC Advanced Grant aiming to bring verification technology to professional mathematicians. This project ends on 31 August 2023 (extended by a year on account of the pandemic), so it’s surely time to update the community on what has been accomplished. As outlined in the earlier post, our starting point was a growing acceptance of the prevalence of errors in mathematics, along with a small body of formal mathematical developments that had been undertaken in a variety of proof assistants. We would mainly be using Isabelle/HOL, which had been designed to be agnostic as to applications but strongly influenced by the verification needs of computer scientists, not mathematicians. There was a detailed research proposal, as is always required, but our real strategy was simply to push things as hard as we could to see what obstacles we would bump into.
Early days, first formalisations
The proposal called for hiring research mathematicians, who would bring their knowledge of mathematics as it was practised, along with their inexperience of Isabelle/HOL. Their role would be to formalise increasingly advanced mathematical material with the twin objectives of developing formalisation methodologies and identifying deficiencies that might be remedied by extending Isabelle/HOL somehow. The project started in September 2017. We hired Anthony Bordg and Angeliki Koutsoukou-Argyraki (many thanks to Mateja Jamnik for interviewing with me). A third postdoc was required to undertake any necessary Isabelle engineering, and Wenda Li was hired.
One of the tasks for the first year was simply to reorganise and consolidate the Isabelle/HOL analysis library, which had mostly been stolen from HOL Light. But we were also supposed to conduct pilot studies. The team set to work enthusiastically, and already in the first year they created a number of impressive developments:
- Projective Geometry, including Hessenberg’s theorem and Desargues’s theorem
- Quaternions and Octonions
- Irrational rapidly convergent series, formalising a proof by J. Hančl published in 2002
- Effectively counting real and complex roots of polynomials, the Budan-Fourier theorem
- The first formal proof that every field contains an algebraically closed extension
Some mathematical proofs rely on calculations, and these can be extremely difficult to carry out formally. Mathematicians frequently rely on intuition when calculating limits and integrals, for example. The root-counting results mentioned above were an early focus of Wenda (who actually joined in almost every task); they belong to real algebraic geometry, and one objective of that work is an efficient, verified decision procedure for deciding equalities and inequalities between polynomials.
Angeliki wrote up her reactions to Isabelle/HOL from the perspective of a mathematician in her paper Formalising Mathematics – in Praxis.
The next phase: advanced formalisations for Experimental Mathematics
Around this time, Kevin Buzzard had launched his own project on formalising mathematics using Lean. As a number theorist, he brought his own perspective. Earlier researchers had formalised huge proofs such as the odd order theorem, but on the whole they had been working with simple objects far removed from the sophistication of mathematical practice. His paper Formalising perfectoid spaces took the viewpoint that before you can even think about proving theorems, you need to show that you can capture some pretty intricate definitions.
We also understood the need to tackle difficult material, preferably from a wide range of mathematical subdisciplines. Meanwhile, Angeliki noticed that that the journal Experimental Mathematics had announced a special issue on formalisation. We decided to aim for that, with substantial projects:
- Irrationality and transcendence criteria for infinite series in Isabelle/HOL, formalising material from three different research papers: by Erdős and Straus, Hančl, and Hančl and Rucki
- Formalizing ordinal partition relations using Isabelle/HOL, formalising papers by Erdős–Milner, and Jean Larson on intricate constructions involving infinitary Ramsey theory.
- Simple type theory is not too simple: Grothendieck’s schemes without dependent types
We were delighted to see all three papers accepted to the special issue, taking up fully half of the accepted submissions.
Schemes are a fundamental construction used in number theory. Buzzard had expressed astonishment that they had not been formalised in any proof assistant. The problem was simply that a user community consisting of computer scientists had never heard of schemes and had no idea what they were for. (I still don’t.) Buzzard’s own paper in Experimental Mathematics described three separate formalisations of schemes, all using Lean. The first definition had to be discarded due to technical issues related to Lean’s type theory and in particular the distinction it makes between equality and definitional equality.
Anthony led the formalisation of schemes in Isabelle, in which I took part. I recall a great many definitions piled one atop the other, but no technical issues at any point. What’s notable is that many well-informed people thought that schemes could not possibly be formalised in Isabelle/HOL, because it lacks dependent types. The opposite is true: the issues with the first Lean formalisation were caused by dependent types.
Advanced library search
ALEXANDRIA refers to the famous library of Alexandria. Even at the start of the project, Isabelle’s Archive of Formal Proofs (AFP) held a substantial collection. At the moment there are nearly 4 million lines of formal proofs and 741 separate entries. The proposal included the goal of supporting intelligent search of large proof repositories and, more speculatively, somehow using the millions of lines of existing proofs in conjunction with some sort of machine learning technology to assist in generating new proofs. In May 2019 we acquired a new postdoc, Yiannos Stathopoulos, who came with the perfect background to tackle these objectives. After much labour, he and Angeliki produced the SErAPIS search engine, which searches both the pre-installed Isabelle libraries and the AFP, offering a great many search strategies based on anything from simple keywords to abstract mathematical concepts. It is a complex area and we don’t claim to have solved all the problems, but SErAPIS has quite a few users. And Yiannos has much more in the pipeline.
Machine learning experiments
The proposal included the task of Intelligent User Support. How this could be provided wasn’t clear from the outset, but machine learning was already topical and we had millions of lines of formal proofs to use as a starting point.
The team applied themselves to this task with great vigour, aided by other members of the Laboratory, notably Sean Holden and Albert Jiang and by other collaborators outside Cambridge. It is now clear that language models can generate formal proof skeletons and translate informal proofs into formal languages (autoformalisation). One of the many outstanding efforts is reported in the paper Draft, Sketch, and Prove. Wenda Li led a separate effort to generate intermediate assertions, for the automated generation of proofs by refinement. These two papers are a mere foretaste of the tremendous developments now underway.
More and more formalisations
Once you get the hang of it, the task of formalisation becomes routine. Then the choice of the next project is a matter of asking whether one of us understand the mathematics well enough and whether we have sufficient time. It actually becomes tedious to list all the results proved. (There is a complete list on the ALEXANDRIA website.) For example, we formalised Szemerédi’s Regularity Lemma and the Balog–Szemerédi–Gowers theorem with the help of Chelsea Edmonds, a PhD student. She also formalised Lucas’s theorem and Fisher’s inequality, and has been building the first formalisation of combinatorial block design theory.
Many of the projects described above (and others not mentioned) involved the work of interns who visited the Computer Laboratory, financially supported by the project and in many cases by Cambridge Mathematics Placements.
Angeliki has pointed out that “we have formalised results by two Fields medalists (Roth and Gowers), an Abel prize winner (Szemerédi) and of course Erdős too!”
Scientific contributions
The most striking and unexpected discovery was that there really seem to be essentially no limits to what we can formalise. I was sure we would run into no-go areas, but this never happened. We aimed for breadth and found that we could handle combinatorics, extremal graph theory, algebra, analytic number theory and everything else we tried.
One particular scientific question is the need for dependent types. Anthony has shown that there are arguments in both directions, presenting straightforward techniques for expressing dependent types within the simply typed language of Isabelle/HOL. Meanwhile, issues caused by intensional equality in Lean continued to show the brittleness of that framework.
Our work also provides further evidence for the thesis that simple type theory (and therefore, also Zermelo set theory) is adequate to formalise mathematics excepting that part that refers to set theory explicitly. Since simple type theory is essentially the formalism of Whitehead and Russell in their Principia Mathematica, we reach the surprising conclusion that they were correct: their logic is indeed strong enough to formalise more or less the whole of mathematics.
The field as a whole has advanced tremendously, driven also by the huge and enthusiastic Lean community. One sign of progress is the famous list of 100 rather arbitrary but notable theorems. It has taken a long time, but now 99 of the 100 theorems have been formalised in one system or another, with Isabelle and HOL Light tied at the top with 87. There’s only one left: Fermat’s Last Theorem.