What is the point of computers? A question for pure mathematicians

I thank the Lean prover community for welcoming me, a mathematician with very little programming experience, into their community back in 2017, and also for reading and giving extensive comments on a preliminary version of this article. Patrick Massot in particular sent many helpful comments on a first draft. I thank Assia Mahboubi and Manuel Eberl for giving advice on the Coq and Isabelle/HOL code in this paper, and to both them and Jeremy Avigad for helpful historical comments. Finally I would like to effusively thank Leonardo de Moura for writing my favourite computer game, and Mario Carneiro for teaching me how to play it.

Consider the problem of proving from first principles that if $x$ and $y$ are real numbers, then $(x+y)(x+2y)(x+3y)=x^{3}+6x^{2}y+11xy^{2}+6y^{3}$. We all know that the real numbers are a commutative ring, so let us assume that fact. The question now becomes how to use the axioms of a commutative ring to prove the equality that we want. How many lines would a proof from first principles be? Surely not too many! We apply distributivity a few times to expand out the brackets on the left hand side, and then of course it just becomes a matter of tidying up and equating terms. As humans we do not think too much about the tidying-up process, however if you try proving this in a theorem prover then you will discover that actually it is a combinatorial nightmare. For example there is a step in the proof where where we need to prove something of the form

using only the laws of commutativity and associativity of addition. Humans apply a principle to justify this step, not an axiom, and indeed proving such a triviality using only the axioms of a ring is surprisingly fiddly. There is also the issue of turning things like $x((2y)x)$ into $(2(x^{2}))y$ and so on.

The very early theorem provers had very limited ability to apply principles, meaning that proving results such $(x+y)(x+2y)(x+3y)=x^{3}+6x^{2}y+11xy^{2}+6y^{3}$ would need to be done manually, meaning something like a 30 line proof. If such a triviality hides 30 lines of axiomatic mathematics, imagine what is hidden behind claims of the form “The function $f$ is clearly $O(x^{-2})$ for $x$ large”? It is one thing writing a computer proof assistant – it is quite another one to write one which scales to do the kind of things which we humans do intuitively. For this and other reasons, many of the earlier formalisation achievements of the 20th century were mathematically trivial. In particular, there were many proofs of the irrationality of $\sqrt{2}$ and of the infinitude of primes, but these were being used as benchmarks for the systems.

In the final two decades of the 20th century, computer provers began to appear which had new functionality. In these later systems, users could write “tactics”. Tactics are computer code which assembles axiom applications together into principles. For example in a modern prover like Lean, $(x+y)(x+2y)(x+3y)=x^{3}+6x^{2}y+11xy^{2}+6y^{3}$ can now be proved in one line by invoking the ring tactic⁴⁴4See [GM05] for a description of the sort of issues which arise when writing such a tactic.. Tactics allow formalised mathematics to more closely resemble ordinary mathematical practice by making ”obvious” things automatic.

In 2004, a team comprising of Jeremy Avigad, Kevin Donnelly, David Gray and Paul Raff formally verified the prime number theorem, in the Isabelle/HOL system. The proof they formalised was the Erdős–Selberg “elementary proof”. The work used inputs from both arithmetic and basic real analysis. Of course calculations involving growth of functions which look easy on paper still took time and effort to formalise. Manipulation of inequalities which to humans look easy need to be done either by hand or via a Fourier–Motzkin elimination tactic in a theorem prover. The reason that the Erdős–Selberg proof was preferred to the traditional complex analysis proof was that at that time Isabelle/HOL had no complex analysis library at all.

What we conclude is that by 2004, more serious undergraduate and MSc level material was now in theory accessible to these systems, at least in some areas of mathematics. We also see that we are at a stage where libaries of proofs in distinct areas of mathematics are able to interact with one another.

In 2009 John Harrison formalised the complex-analytic proof of the prime number theorem in the HOL Light theorem prover [Har09a], motivated in part by the fact that HOL Light already had a theory of complex analysis including Cauchy’s integral formula. In 2016 Mario Carneiro formalised the Erdős–Selberg proof in Metamath, a set theory based prover which has essentially no tactics; as you can imagine this was a heroic effort.

Thus the Prime Number Theorem became some kind of a poster child for formalisation. One can understand why – it was a celebrated theorem in mathematics, the proof is not at all trivial, and any formalisation in a theorem prover demonstrates that the prover is capable of reasoning about both the discrete and the continuous simultaneously.

As may be becoming apparent to the reader however, one reason that the result was being independently formalised in several theorem provers was that it is extremely difficult to translate a proof written in one of the systems to a proof in another system. One issue is that different systems might have different foundations; for example HOL Light and Isabelle/HOL are type theory systems, and Metamath is a set theory system. Another issue is that even if two proof systems have very similar foundations, they might have different idioms; different libraries in different systems could be set up to do the same thing in very different ways. Without getting too technical, in order for these computer proof systems to work one has to have some kind of a method for moving between structures “behind the scenes” – for example the reals are a field, and hence they are an additive group (and a multiplicative monoid), and in particular one wants all theorems about additive groups such as $0+a=a$ to apply instantly to fields such as the reals without any fuss. Humans of course have no problems with this, but in a computer proof system one needs some kind of infrastructure which is making this happen automatically, and if different systems are doing this in different ways then of course this makes automatic proof translation much harder.

Thus it came as a shock to me when in 2020 Mario Carneiro announced that he had used his Metamath Zero project [Car21] to port the Metamath proof of the prime number theorem to Lean. The two systems are about as far apart as it is possible to be – Metamath uses set theory as a foundation and Lean uses type theory, for example. Metamath proofs are typically far more low-level, with limited automation available, whereas typical Lean proofs are very tactic-heavy. However the system worked, and produced code which compiled; it was of course also unreadable. It was tens of thousands of lines of completely unmotivated primitive code defining variables and applying basic principles of logic, with no comments. In fact it was a wonderful example of something which satisfied a formal definition of “being a proof”, whilst in some sense imparting no information whatsoever to the human reader other than the fact that the theorem was true.

Of course if computers begin to write proofs by themselves, they might all look like this, at least at first.

The four colour theorem (formerly the four colour conjecture) was a notorious problem in graph theory raised in the 1850s and which remained unresolved for over 100 years. One formulation of it is the assertion that the vertices of every planar graph can be coloured with four colours in such a way that no two adjacent vertices share a colour. The statement is an elegant combinatorial problem, and it came as a shock to some in the mathematical community that the proof, announced by Appel and Haken in 1976, used a computer in an essential way. Appel and Haken constructed a collection of 1834 graphs with the property that a minimal counterexample must contain one of these graphs as a subgraph, but that conversely no graph containing one of these 1834 graphs as a subgraph can be a minimal counterexample. The verification of these claims was done using a bespoke computer program which, in those days, took over a month to finish running. The Appel–Haken proof was an outlier because whilst the principle of the proof was possible to understand, the details were too difficult for a human to follow in practice; one billion case splits (this is what the computer part of the proof looks like) is not something which humans can do manually and accurately within a reasonable time frame. The proof relies, essentially, on a computer calculation and hence it relies on the correctness of the computer code. Small bugs in computer code are of course commonplace, although it of course could be added that small bugs in human-written proofs are also commonplace. However the mathematical community is well-equipped to discover and fix small bugs in human-written proofs, and was perhaps rather less well-equipped to verify the correctness of computer code, especially in 1976.

In 2004 Georges Gonthier finished a formal verification of the Appel–Haken result – more precisely he formalised the 1997 Robertson–Sanders–Seymour–Thomas variant of the argument [Gon07]. The work comprised of 60,000 lines of code written in the Coq proof assistant. In particular it completely dwarfs the prime number project discussed in the previous section. It contains a complete formalisation of the theoretical part of the work – formal proofs of results in topology (to reduce the statement about arbitrary planar graphs to one of a discrete combinatorial nature) and graph theory – whilst also formally verifying the computer calculation necessary to finish the proof. Note in particular that (as in the proof of the prime number theorem) much of the work comprised of writing foundational material rather than formalising the proof itself.

It is interesting to note that the process of formalisation led to simplifications in the argument. For example Gonthier developed a theory of what he called combinatorial hypermaps, which greatly reduced the amount of topology needed in the proof, and in particular removed the dependency of the argument on the Jordan Curve theorem. Gonthier developed some original mathematics as part of the work – for example he isolated a combinatorial criterion for his hypermaps which was equivalent to planarity.

Naively, it looks like in this case we are replacing one “proof by computer” with another one, however this is missing the point. Firstly, the Coq formalisation covers not just the Appel–Haken computer code, but also all of the rest of the Appel–Haken argument. Secondly, one can view the formal verification as an independent check of the proof. Finally, instead of having to trust the code written by Appel and Haken and which few people have read, we are instead having to trust code written by the authors of Coq. Coq has been around for a long time (the first version was written in 1984), has a small kernel, and the system has many users. A bug which meant that Coq could incorrectly claim that an unproved theorem was true would be unlikely to manifest itself in just one project and is far more likely to ultimately be discovered. In contrast, the Appel–Haken code is a bespoke piece of code with few users so arguably bugs are more likely.

Gonthier wrote a very informative piece [Gon08] about his work for the Notices of the American Mathematical Society (including an exposition of the theory of hypermaps), as part of the November 2008 issue; this issue was devoted to formal verification of mathematics in a computer proof system and provides an excellent survey of the field as it then stood.

The odd order theorem is the theorem that any finite group of odd order is solvable. In 2013 a team of 15 people led by Gonthier formally verified a proof of this theorem in Coq [GAA⁺13]. This piece of work is notable for several reasons. Firstly, the proof is very long; a complete argument (modulo the basics in group and representation theory) is presented in the two volumes [BG94] and [Pet00]. Secondly, we have moved way beyond MSc level mathematics here – this work was one of the reasons that Thompson was awarded the Fields Medal in 1970. The proof is a very delicate argument in finite group theory, much of which involves analysing the structure of a minimal counterexample and ultimately showing that it cannot exist. The Coq proof involved formalising both of the books mentioned above, plus of course all the background material in group theory, representation theory, Galois theory and number theory; indeed, formalisation of the background material took up much of the six years which the authors spent on the proof. Figuring out how to handle such a large-scale formalisation project was also a non-trivial task.

It is perhaps worth stepping back and asking how work like this contributes to human understanding. The naive answer to this is “it guarantees that the human proof is correct”. However, in my opinion this is not the main contribution. Humans were well aware even back in the 1960s that the proof was correct – had there been any doubt, Thompson would not have got the Fields Medal. What the formalisation work shows us that theorem provers have now become able to operate at this kind of scale. Entire books of mathematics can now be formalised in one system without the system running out of memory or grinding to a halt. On average, one line of mathematics in [BG94] or [Pet00] corresponded to five lines of computer code, so we learn that by 2013 the so-called “De Bruijn factor” for this kind of mathematics is around 5. However this ratio should not be taken too seriously: in parts of the argument the ratio is essentially one, and in other parts it is much larger. Note also that this factor may vary considerably between theorem provers.

We also learn that large formalisation projects such as this are a very effective way to motivate development of foundational mathematics libraries. One consequence of this formalisation project was that Coq developed a very solid library of undergraduate-level algebra which can of course be used (and is used) for other projects.

The write-up [GAA⁺13] of the odd order work is an interesting read. Some sections concentrate on the mathematics or the history, but there is also a discussion about constructive mathematics, something which I felt should have nothing to do with the work, and also about implementation issues, something else which mathematicians typically do not ever have to think about. For example, one observation made in section 3 was that many theorems involving two or more finite groups would usually be formalised assuming that these groups were both subgroups of some larger ambient finite group $X$. This can be done without any loss of generality of course, because given two groups $G$ and $H$, they are both subgroups of $G\times H$. Why is this observation important? This is an implementation issue – the domain of the computer scientist. Working with subgroups rather than groups might be easier, or nicer, when it comes to actually implement certain theorems in the theorem prover. It is worth noting however that such a trick does not work more generally: for example in algebraic geometry one uses the category of commutative rings with 1, and morphisms by definition send 1 to 1. If $R$ and $S$ are general commutative rings with 1 then there is in general no morphism of rings from $R$ to $R\times S$ sending 1 to 1, so one is forced to implement commutative ring theory in a more “traditional” manner. See [Wie21] for how this was done in Lean.

Regarding constructivism – the authors of the work put in a lot of effort to keep their proof “constructive”, for example the avoidance of all uses of the complex numbers when setting up the basics of representation theory. The complex numbers do not have decidable equality, meaning that there is in general no algorithm for proving that two constructively defined complex numbers are equal (for example, one can evaluate a definite integral numerically and observe that it seems to be $0$ to 1000 decimal places, but there is not some generic algorithm which we can apply to an arbitrary integral in order to decide whether or not it equals $0$). This means that in constructive mathematics, where the law of the excluded middle cannot be assumed, one cannot do a case split on whether $z=0$ or not, if $z$ is a complex number, and more generally plenty of constructions become noncomputable and hence much harder to reason with constructively. These design choices thus increase the amount of work needed to get representation theory working. I had thought that constructivists had died out in the early part of the 20th century. It turns out that they are alive and well, and typically working nowadays in computer science departments. One reason for this is that constructivism plays an important role in the theory of programming languages. Reluctance to use the law of the excluded middle is to a certain extent a cultural decision. However there are also situations where working constructively enables a computer proof system to prove certain results “automatically” (for example by an explicit computation). Whilst working constructively may have been feasible for a project about finite groups, the law of the excluded middle is used throughout most modern research level mathematics and it is not really feasible to work constructively when doing the kind of mathematics which is happening nowadays in mathematics departments. However it is also worth stressing that most modern proof assistants have no problems with the law of the excluded middle, the axiom of choice, and other non-constructive axioms – they are available, if you want them. Certain proof strategies are ruled out if one chooses to work nonconstructively, but one can counter this by writing new tactics specifically designed to do computations in fields such as the real and complex numbers. Nonconstructive axioms are used extensively in Lean’s mathematics library mathlib, for example.

The Kepler conjecture states that the face-centred cubic packing is the densest way to pack congruent spheres in 3-space. Hales and Ferguson proved the conjecture in 1998; it had at that point been open for over 350 years (it was raised by Kepler before Fermat proposed his Last Theorem). Part of the Hales–Ferguson proof involved the checking of over 23000 non-linear inequalities on a computer; another part involved a computer classification of all tame graphs. Other computer calculations were also involved. In this respect the proof is similar to the Appel–Haken proof of the four colour theorem; computations need to be carried out which are simply far too great for humans to do in a reasonable time frame.

Because the result was regarded as important, the referees felt duty-bound to attempt to check the computer part of the proof in some way; however ultimately they gave up, and in [HAB⁺17] Hales states that the paper was published (in the Annals) without complete certification from the referees. In 2003 Hales announced a project to formally verify the proof using computer proof systems. Hales used a combination of HOL Light and Isabelle/HOL, and the project turned into an international collaboration, with 22 authors listed on the final paper. The formalisation project took around 12 years to complete, and comprised over half a million lines of code. Just as for the other projects in this section, one of the main benefits of the work to the formal proof community is that HOL Light’s standard library grew to include theorems such as the Brouwer fixed-point theorem, the Krein–Milman theorem and the Stone–Weierstrass theorem.

In 2017 Hales gave a talk [Hal] at the Newton Institute where he tells the story of the Kepler proof, and explains a vision for the future of formalised mathematics. This talk was, for me, the turning point, and was one of the main motivations behind the work described in the following subsection.

The previous formalised results all have something in common. Whilst some of them represent truly deep mathematics, all of the formalised proofs involve reasoning about objects which are in some sense elementary (planar graphs, prime numbers, finite groups, spheres). Furthermore, most (but not all) of the formalising done prior to 2017 was being done by computer scientists. In Hales’ talk linked to above, he coherently argued that for further progress in this area, this state of affairs had to change. At that time I had only just begun to dabble with computer proof assistants and my initial plans were to attempt to integrate them into my undergraduate teaching. However Hales’ arguments resonated with me, and within a few months I found myself working with undergraduates at Imperial College, formalising the definition and basic properties of schemes in the Lean theorem prover. This project involved developing basic theories of localisation of rings and of sheaves on topological spaces; however it was relatively straightforward (modulo poor design decisions; the reader interested in more details can see them in [BHL⁺21]). I was thus shocked to discover afterwards that schemes – such a basic notion in algebraic geometry – had not been previously formalised in any other computer proof system! Furthermore, the project made it quite clear to me that formalising far more heavyweight mathematical objects should easily be possible.

In late 2017 Patrick Massot (a topologist) and myself independently came up with the idea of formalising perfectoid spaces; the topic was in the air because it was at that time an open secret that Scholze was going to be awarded a Fields Medal for his invention/discovery of the concept and its applications to arithmetic geometry. I knew the mathematical definition, having dabbled in the area myself, and when Johan Commelin, another arithmetic geometer, appeared in the Lean Zulip chatroom in 2018 the three of us decided to go for it. Around 16000 lines of code and eight months later, we had a formalised definition; one could summarise the work as a computer formalisation of the single line of mathematics “let $X$ be a perfectoid space”.⁵⁵5In the odd order formalisation, the de Bruijn factor (ratio of lines of computer code to lines of human text) was around 5. Here one could argue that it is 16000. However one could of course also argue that it might well take several thousand lines of human text to define a perfectoid space in full.

The work was of course partly intended as a public relations stunt; computer scientists were well aware of the existence of computer theorem provers, however mathematicians seemed not to be, and this was an attempt to make them notice. The plan was a success – the project did seem to raise the profile of computer theorem provers within the mathematics community. Note however that we did not construct any examples of perfectoid spaces other than the empty perfectoid space⁶⁶6To prove that the empty set can be given the structure of a perfectoid space, one needs to check that an arbitrary product of trivial topological rings is the trivial topological ring., and all three of us were well aware of the problems preventing us from formalising any of Scholze’s serious theorems about perfectoid spaces at that time; we were missing so many of the prerequisites. As with previous projects, one tangible gain from the work was the growth of the mathematics library of the system in question. Most of the results in Bourbaki’s General Topology ended up as part of Lean’s mathematics library mathlib as a result of this project, as well as plenty of results in topological algebra, and it also motivated the beginnings of a theory of valuations and discrete valuation fields.

One can consider the perfectoid space work as in some sense being orthogonal to what was usually being attempted in a theorem prover. Many of the prior results highlighted in this section are proofs of long and complex theorems about relatively simple objects. The proof that the empty set can be given the structure of a perfectoid space is a very simple theorem about a much more complex concept. Of course the natural next question is whether computer proof systems can prove complex theorems about complex objects. One year after the perfectoid space project, we began to find out.

Clausen and Scholze have been developing a theory of condensed mathematics. A condensed set is a variant of a topological space. The main insight is that condensed objects may have better homological properties than topological objects (for example the category of condensed abelian groups is an abelian category, whereas the category of topological abelian groups is not). They hope that these ideas will enable techniques in homological algebra to apply to new areas of analytic geometry. At the end of 2020, Scholze approached me and asked if we had had a study group on the work at Imperial; I answered that we had. Scholze then asked whether we had looked through all the details of the proof of Theorem 9.1 of [Schb]; I answered that we had not. Scholze then remarked that he had had the same response from other mathematicians, and raised the possibility that perhaps nobody other than himself and Clausen had ever read the proof carefully. Furthermore he suggested that perhaps this might remain true even after the refereeing process. The reason he was concerned about this was that, for Scholze, this was the theorem that the entire theory stood upon. The proof was very technical; it built upon a more “elementary” but rather unwieldy intermediate result, Theorem 9.4 of [Schb]. Scholze agreed to challenge the formalisation community to prove his Theorem 9.1 in a blog post [Schc], later published as [Sch21]. Although the challenge was to the formalisation community in general, it seems that only the Lean community responded; this is perhaps unsurprising, as (for perhaps only for sociological reasons) it has come to be the case that mathematicians interested in “the kind of mathematics which wins Fields Medals” and also interested in theorem provers tend to gravitate towards Lean.

Johan Commelin became the de facto leader of the formalisation process, with Patrick Massot supporting him in making a blueprint [CM] of the strategy (that is, a carefully-written roadmap) and a team of algebraic number theorists, arithmetic geometers and other mathematicians (Riccardo Brasca, Damiano Testa, Filippo Nuccio, Adam Topaz, myself, Patrick Massot, Bhavik Mehta…) then began working on the project, with the occasional help from people with a computer science background such as Mario Carneiro. Within six months the team had grown to over ten people and we had formalised a complete proof of Theorem 9.4 (see [Cas]). At the time of writing we have not deduced Theorem 9.1, but it is only a matter of time. A second blog post [Scha] by Scholze indicates his thoughts on the matter; in particular we see that he is now far less concerned about the situation regarding the correctness of the results. Furthermore, Scholze has indicated (personal communication) that the process has enabled him to better understand what powers the proof, and Commelin not only learnt the mathematics as part of the process, but also simplified the argument in several places, most notably in the removal of the dependency of the argument on prior work of Breen and Deligne.

For me, this represents substantial evidence that now any pure mathematics can be formalised in theorem provers – both in theory, and in practice. It takes time, but it is possible. The formalisation of the work led both to better understanding of it, and to simplifications of the argument. Also worth mentioning is that, as in many other formalisation projects, a substantial amount of time was spent formalising background material (for example the theory of normed groups and the theory of profinite spaces). As the libraries of the provers get better and start to contain the kind of material which working mathematicians take for granted, there will be fewer of these “startup costs”.

There are plenty more examples of serious formalisation efforts which we do not have the space to cover. We list some examples here. Gouëzel formalised the basic definitions of $C^{k}$ and $C^{\infty}$ manifolds in Lean, extending earlier work done in Isabelle/HOL. Mahboubi and Sibut-Pinote proved irrationality of $\zeta(3)$ in Coq [CMSPT14] and Eberl proved it in Isabelle/HOL [Ebe19a]. Mahboubi has also done extensive work on rigorous numerical values of integrals in Coq, and also in Coq Bertot, Rideau and Théry formally verified the first one million decimal digits of $\pi$ [BRT18]. Eberl has formalised much of Apostol’s textbook on analytic number theory in Isabelle/HOL [Ebe19b]. Han and van Doorn proved independence of the continuum hypothesis in Lean [HvD20]. Immler formally verified Tucker’s calculations used to verify the existence of the strange attractor [Imm18]. Mehta and Dillies formally verified Szemerédi’s regularity lemma and Roth’s theorem on arithmetic progressions in Lean, and Edmonds, Koutsoukou-Argyraki and Paulson verified them in Isabelle/HOL [EKAP21]. The Poincaré–Bendixson theorem was formalised by Immler and Tan [IT20] in Isabelle/HOL; note that the usual proof as understood by mathematicians relies on drawings, and formalising drawings can be hard work. The Ellenberg–Gijswijt resolution of the cap set conjecture was verified in Lean by Dahmen, Hölzl and Lewis [DHL19]. Commelin and Lewis constructed Witt vectors and showed that $W(\mathbb{F}_{p})=\mathbb{Z}_{p}$ in [CL21]; this work is interesting because not only did they formalise the delicate mathematics involved, they also wrote tactics which would enable them to reduce various questions to the universal case in a painless manner. Finiteness of the class group of a global field was proved in Lean by Baanen, Dahmen, Narayanan and Nuccio in [BDNdC21] (it still astonishes me that this result, special cases of which were known to Gauss and which is a standard theorem in an undergraduate mathematics degree, was formalised in a proof assistant for the first time in 2021; this development is a demonstration of how the mathematical interests of the formalisation community now is encompassing work which people in mathematics departments might view as “mainstream”).

There is also work in progress (at the time of writing). Teams of people who collaborate on the Lean Zulip chat [Zul] are currently working on a proof of Fermat’s Last Theorem for regular primes, and on Smale’s theorem that it is possible to evert a sphere. A general project to formalise many basic results in the theory of schemes is also underway.

Mathematicians nowadays are used to seeing the word “set” floating around when it comes to basic definitions. For example, we are told that a group is a set equipped with a multiplication such that some axioms hold. We’re not told what a set is though; a course on ZFC set theory tells us a list of properties which sets have, but they don’t tell us what a set is. Indeed in this context the word “set” has no formal definition; it is simply the generic term for an object in our model of the axioms of mathematics, and we build other mathematical objects on top of this basic object.

In definitions such as the definition of a group, the word “set” is being used to mean no more than “collection of elements”. In type theory, the role of a “collection of elements” is played by the type. A type is a collection of terms. The definition of a group in type theory: a group is a type equipped with a multiplication such that some axioms hold. The only difference is the notation: the set-theoretic $a\in X$ is replaced by the type-theoretic a : X.

As mentioned above, those of us who have been to a set theory class will know that, when using set theory as a foundation of mathematics, everything is a set. For example the elements of a group are, strictly speaking, also sets, so one could in theory talk about their elements too, although within the context of group theory such questions would not be mathematically meaningful, as they are not isomorphism-invariant. In type theory this is not possible; the elements of a type are called terms, and in general terms are not types. In type theory, everything is a term, and every term has a type, but not every term is a type. For example, in type theory $37\pi^{2}$ is a term, whose type is $\mathbb{R}$, the type of real numbers. We write $37\pi^{2}\,:\,\mathbb{R}$. However $x\,:\,37\pi^{2}$ does not make sense, because $37\pi^{2}$ is not a type. In a set-theory based theorem prover, questions such as asking if the trivial group is an element of the Riemann zeta function would make sense but its meaning would be unmathematical – it would depend on implementation decisions. Type theory thus provides a basic check that what you are writing has mathematical meaning.

In a type theory system, the type $\mathbb{R}$ is still built from $\mathbb{Q}$ as equivalence classes of Cauchy sequences, or via Dedekind cuts, or as another of the standard constructions; the mathematical part of the story is identical to the set theory set-up, it is just that the language used is slightly different (types and terms, rather than sets and elements).

One difference between types and sets however is that types don’t mix: distinct types are disjoint. This has practical advantages when formalising mathematics because it provides a strong check that the mathematics you’re typing makes sense: in type theory, if $g$ is an element of the group $G$, then the only type that $g$ can ever be a term of is $G$.

This approach does however have consequences which can initially come as a shock to a mathematician. For example one could make a type representing the positive reals $\mathbb{R}_{>0}$ and a type representing the reals $\mathbb{R}$, but if a term $x$ had type $\mathbb{R}_{>0}$ then $x$ itself would not strictly speaking have type $\mathbb{R}$; I stress again that every term has a unique type. To make a term of type $\mathbb{R}_{>0}$ one has to give two pieces of data: a real number, and a proof that it is positive. A term of type $\mathbb{R}_{>0}$ is an object corresponding to this pair, so strictly speaking it is not a real number, and a type theory based system will hold you to this. However of course there is a canonical map from $\mathbb{R}_{>0}$ to $\mathbb{R}$ – you just throw away the proof. More generally, a type theory system could well have a coercion system, consisting of a collection of “invisible functions” mapping types to other types in the way which mathematicians would expect. For example given a term of type $\mathbb{R}_{>0}$ it might well be possible to feed it into a function which is expecting a term of type $\mathbb{R}$; the system will just throw away the proof of positivity and use the underlying real number anyway. Mathematicians use these invisible functions everywhere, often without noticing. We have already mentioned above that in a foundational system the real numbers need to be built using one of the standard constructions, for example via Cauchy sequences. In particular a rational number is not literally a real number. However, taking Lean as an example, if one has a term x : ℚ then one can simply write x : ℝ to get the corresponding real number, although a careful inspection of the corresponding term will unearth the fact that the real number is actually called ↑x, indicating that a coercion has been applied. The coercion is a ring homomorphism, and Lean has a “normalise casts” tactic [LM20] which knows this and will apply theorems such as ↑(x+y)=↑x+↑y and ↑(x*y)=↑x*↑y automatically (before this tactic had been written, doing mathematics which involved switching between the naturals, integers and rationals could be quite frustrating because of these invisible maps). In summary then, type theory forces you to think more precisely about the actual objects you are working with, however tactics can be used to manipulate these objects the way we usually manipulate them. Learning how to “steer” mathematics in a theorem prover this way simply comes from practice.

I have already mentioned that in a type theory system the definition of the real numbers is the same as in a set theory system – it is Cauchy sequences, or Dedekind cuts, or whatever your favourite construction of the reals is. Similarly the usual definitions of the rationals and integers as quotients work just as well in type theory as they do in set theory. But one place where the type-theoretic and set-theoretic foundations of mathematics differ is in the definition of the natural numbers. The natural numbers are a foundational object in mathematics – they are typically the first example of an infinite object to be born – so it is perhaps unsurprising that different foundational systems will treat them in different ways.

In ZFC set theory, the existence of the set of natural numbers is postulated as an axiom, namely the axiom of infinity. Type theories such as Lean’s instead allow the user to define custom inductive types. Such types include the naturals and other recursively-defined constructions. Implementation details of this so-called calculus of inductive constructions [CP88] differ between systems; the rest of this section explains details which are specific to Lean’s type theory, but much of what I say applies to Coq and Agda, other popular type theory provers.

In Lean, the definition of the naturals looks like this:

This definition says “zero is a natural number, the successor of a natural number is a natural number, and that’s it”. As one might guess, this inductive construction can be used to construct far more exotic types, but one can show that any type which can be defined using the rules of the calculus of inductive constructions corresponds to a set which can be built using the usual axioms of set theory.

Let us see what goes on under the hood when the naturals are defined as an inductive type. When such a definition is made, a new type nat appears in the system, as does the term nat.zero and the function nat.succ : nat → nat. The latter terms are called constructors: they are ways to make natural numbers. However one more thing also appears, namely the eliminator for the type – the object which enables the user to construct functions whose domain is the naturals and whose codomain is something else. It represents the idea that the only way that one can construct naturals is via nat.zero and nat.succ, and it states that to define a function out of the naturals, it suffices to (1) say where nat.zero goes, and (2) to say where nat.succ n goes, given where n went. In other words, it is the principle of recursion.

So this is how new inductive types are born in Lean; after their definition they, together with their constructors and eliminator, are automatically added by the proof assistant to the system as new constants, or axioms, or however you would like to think of them. There are of course precise rules telling us the exact form of the eliminator for a given inductive type; we do not go into these here. From a foundational point of view this approach, where new axioms appear “by magic” as types are constructed, is very different to the set-theoretic viewpoint, however in [Wer97] it is shown that type theory with these constructions is equiconsistent with set theory. The strategy of the proof is to make a model of set theory within type theory, and to make a model of type theory within set theory. For a more precise statement, one has to be more precise about exactly what kind of type theory one is working with. For example Mario Carneiro’s MSc thesis [Car] shows that Lean’s type theory is equiconsistent with ZFC plus countably many inaccessible cardinals.

It is worth noting, and quite amusing, that equality itself is defined as an inductive type in many type theory systems. This is in contrast to set theory, where equality is typically considered as part of the logic. Indeed, equality in type theory is generally more subtle than in set theory. Here is Lean’s definition of equality:

The slightly unnerving X → X → Prop, bracketed as X → (X → Prop), means that equality is a function which takes in an element of X and outputs a function which takes in an element of X and outputs a Proposition, that is, a true-false statement. In other words, if a and b are terms of type X then eq a b is a true-false statement. Using the usual notation a = b for eq a b, we see that equality of terms of a type X is an inductive type with one constructor, namely eq.refl a, a proof that a = a. It turns out that from this definition we can prove all the usual properties of equality! The eliminator for the equality type is the substitution property, that if $a=b$ then given a term of type $P(a)$ we can get a term of type $P(b)$. It is a rather pleasant game to go on from this to deduce that equality is both symmetric and transitive (for more details on this see for example [Buzb]). Of course, whilst it is of interest to some to see how basic properties of equality can be proved within a type theory system, it is also worth stressing that to use a computer theorem prover one does not have to know anything about them.

Lean and Coq both use a version of type theory called dependent type theory, so it is perhaps worth taking some time to explain what a dependent type is. Imagine $X$ is a geometric object, for example a real manifold. Say that we have a vector bundle on $X$, that is, for each point $x$ of $X$ a vector space $V_{x}$ (which varies smoothly with $x$ in some appropriate sense). A section of this bundle is a function which takes as input a point $x$ in $X$ and outputs an element of $V_{x}$. From a foundational point of view there are two ways to think about such a section. One could regard this section as a function from $X$ to the disjoint union of the $V_{x}$, sending $x\in X$ to an element of $V_{x}$. Alternatively one could regard it as a slightly stranger kind of “function” which has domain $X$ but whose codomain varies according to the input. There are times in mathematics when taking the disjoint union of the codomains is a natural thing to do – for example in the example above, the disjoint union of the $V_{x}$ is naturally a space $V$ sitting above $X$. However there are also times when taking the disjoint union is quite unnatural. For example, in algebraic geometry one way of defining the sections of the structure sheaf on an affine scheme $\mathrm{Spec}(R)$ is functions which send a prime ideal $P$ of $R$ to an element of the localisation $R_{P}$ of $R$ at $P$, and the disjoint union of the $R_{P}$ as $P$ varies over the prime ideals of $R$ has no natural algebraic structure. The set or type consisting of the disjoint union of these local rings is typically not part of the mental model which an algebraic geometer has when describing these sections.

These kinds of “functions” which have a well-defined domain, but a codomain which can vary according to the input, are called dependent functions. Not all proof assistants have such functions; for example Isabelle/HOL (a powerful proof assistant which contains a lot of analysis and analytic number theory) and various other HOL systems do not have them, which means that certain constructions in geometry are more convoluted than in Coq or Lean. See for example [BPL21], which defines schemes in Isabelle/HOL but which has to build a new implementation of ring theory from scratch in order to do so.

Let us take a look at some examples of what mathematics looks like in a theorem prover based on type theory. I give these examples mainly to convince the reader who has been brought up using the language of set theory that there really is very little difference.

Here is what the claim that $\sqrt{2}$ is not rational looks like in Isabelle/HOL:

theorem sqrt2_not_rational:
  "sqrt 2  "

You can see the proof on Isabelle’s Wikipedia article [Wik]. The fact that 2 is a term of a type and not a set, or an element of a set, is invisible.

Here is some more advanced mathematics, written in Coq:

Lemma prod_Cyclotomic n :
(n > 0)%N -> \prod_(d <- divisors n) ’Phi_d = ’X^n - 1.

This is the statement that the product of the $d$th cyclotomic polynomials over $d\mid n$ is $X^{n}-1$. Note the hypothesis $n>0$, an assumption which a human would typically omit; computers are very picky with such “edge cases”.

Here is the definition of a perfectoid ring in Lean, taken from the Lean perfectoid spaces website [BCM] which accompanies the article [BCM20].

The comment at the top of the code is the “docstring” for the code – this is the human-readable explanation of what the Lean definition perfectoid_ring represents, and this docstring is visible when you hover your cursor on the word perfectoid_ring in some Lean code; if you are running the code in an IDE such as Microsoft VS Code then right-clicking on this word will jump you to the definition.

The Lean definition pretty much coincides with the human definition. If $R$ is a Huber ring which is a Tate ring (these are technical properties of topological rings), then we say $R$ is a perfectoid ring if it is complete, uniform and satisfies a couple of technical properties. The point to observe is that the computer code is no more or less difficult than the human definition.

In my experience, mathematicians often have very little interest in the technicalities of the logical foundations of their subject – they cannot list the axioms of set theory, but they know from experience what is “legal mathematics”. The controversies of the early 20th century about whether nonconstructive methods are allowed in mathematical proofs have long ago died down; working mathematicians use the law of the excluded middle all over the place, and many use the axiom of choice in some form or another (indeed countable dependent choice can be invoked almost without one noticing). A typical research mathematician will have gone to at most one course on the foundations of mathematics; in such a course one typically learns that Zermelo–Frankel set theory with the axiom of choice, or ZFC, can be used as a foundation for much of mathematics. Indeed it can be used for essentially all of mathematics up until the 1960s; however Grothendieck’s super-general cohomology theories developed in SGA4 introduced a new “axiom of universes” (the assertion that every set is an element of a set which is a model of ZFC). This axiom cannot be proved from the axioms of ZFC, by Gödel’s theorem. The original proofs of the Weil conjectures in theory used this axiom in the weak sense that at the time the only reference for étale cohomology was SGA4. However Deligne and others point out in SGA4$\frac{1}{2}$ that the theory of étale cohomology, and hence the proof of the Weil conjectures, can be set up within ZFC alone. Readers interested in the contortions that one has to go through in order to do this can look at the Set Theory section of the Stacks project, for example here [Sta18, Tag 000H]. For a more extreme example, see section 4 of [Sch17], where we see a Fields Medallist forcing a more elaborate theory into ZFC.

My personal opinion is that whilst ZFC was a wonderful foundation for much of early 20th century mathematics, the lack of a universe axiom now means that it is becoming more and more of an effort to get parts of modern mathematics to fit into it. In books and papers dealing with infinity categories or condensed mathematics it is not at all uncommon to see universes showing up, and I do wonder whether now it is time for mathematicians to begin embracing universes, as Grothendieck was encouraging us to do since the 1960s. Coq’s type theory and Lean’s type theory both contain universes as part of the foundations, however mathematicians can choose not to use them if they so desire.

Right now, an author of a textbook or research paper has to decide how much background material to assume, and which techniques they will regard as standard in the arguments they present. In other words, they have to decide where to start, and how fast to go. If a potential reader (for example a new PhD student, or an undergraduate interested in the area) does not have the necessary prerequisites then it will be far more difficult for them to get anything out of the paper.

Computer formalisation offers the possibility of a new kind of mathematical document, where the reader can make the decisions about how much detail is visible. Patrick Massot has been experimenting with such documents. A preliminary version of his vision can be seen at his Sphere Eversion Project web pages [Masa]. This is a project whose main goal is to formalise in Lean a proof of Smale’s theorem saying that a sphere can be turned inside out (or more formally, that there is a homotopy of immersions between the identity immersion of $S^{2}$ in $\mathbb{R}^{3}$ and the antipodal immersion). At the time of writing, the proof is not yet fully formalised, but it is only a matter of time. The blueprint is written in LaTeX, but using plasTeX it has been converted into a web page with live Lean links. Right now these links take you to static web pages containing Lean code, but tools are currently being developed which will change this. Alectryon is a program available for Coq and Lean which can turn compiled code into web pages. Tools like Alectryon will enable us to make documents which will allow links to dynamic web pages displaying anything from mathematical details to interactive pictures, in a human-readable form, and which will allow one to keep digging right down to the axioms, although of course it is unlikely that anyone would like to go down this far.

There are already variants of this idea in existence, Lamport’s idea of a “structured proof” came from a desire to encourage mathematicians to write far more details down in their papers, but one can see why such a proposal would not go down well. Here we can let automation do part of the work for us. The Metamath proof assistant also offers similar functionality already, because Metamath has very little automation and hence drilling down to the axioms is essentially the same as inspecting the proof.

One could also imagine error-free undergraduate textbooks also written in this way, where statements which a student cannot understand (perhaps because they are ambiguous) can be inspected in more details until difficulties are resolved.

One thing that is not going to happen any time soon, is some kind of revolution where all mathematicians start writing all their papers in a formal proof assistant. Whilst one might expect a future where some papers are partially, or even completely formalised in a theorem prover (see for example [GS19], [SB19] and [KHNY21]), this kind of approach will not become the norm any time soon. Faced with this reality, how will formalised mathematics be able to keep up with the frontiers of mathematics?

I have already mentioned Tom Hales’ 2017 “Big Conjectures” talk at the Newton Institute in Cambridge. In the talk [Hal], Hales argues for a formalised version of Math Reviews/Zentralblatt. That is, a website whose role is to formally state the results being announced in the main mathematical journals. Note that such a project is nowhere near as far-fetched as the idea of formalising mathematical proofs in real time; theorem statements are far easier to formalise.

The issue with Hales’ plan, as he points out in the talk, is that to be able to formalise statements of theorems in even a part of modern mathematics such as the Langlands philosophy, one would have to define all of the basic objects which mathematicians in this area use. In the Langlands philosophy this would include, but be by no means limited to, definitions of automorphic forms and automorphic representations, Galois representations, abelian varieties, the rings defined by Fontaine and used to do $p$-adic Hodge theory, schemes, all the cohomology theories used in the area, perfectoid spaces, adeles and ideles,…. The Lean community has over the last few years pushed hard to get some of the main definitions of modern research mathematics into mathlib. At Imperial College alone we currently have Oliver Nash developing the basics of the theory of Lie Algebras so we can talk about centres of universal enveloping algebras, María Inés de Frutos-Fernández developing the theory of adeles and ideles of global fields with an eye on the statements of class field theory, Amelia Livingston developing group and Galois cohomology, Jujian Zhang developing sheaf cohomology with an eye on GAGA, and Ashvni Narayanan developing the basics of Iwasawa theory in her PhD thesis. I have already mentioned the work of myself, Massot and Commelin defining perfectoid spaces. The work of Scott Morrison, Bhavik Mehta, Justus Springer and Adam Topaz has recently enabled us to start developing the theory of sheaves on sites and homological algebra, so cohomology theories are now not too far away. Of course much remains to be done, but we are hoping that the idea of being able to formally state the theorems of Annals and Inventiones algebraic number theory papers in Lean will soon become a reality.

A related project is formalising tags in the Stacks Project. The Stacks Project [Sta18] is a gigantic online database of algebraic geometry, freely accessible online. When printed out, it fills over 7000 pdf pages. Formalising all the proofs in the database would be an extremely arduous task involving many person-decades of work with current technology. In theory it is possible, however one would need a team who were experts in both algebraic geometry and in formalisation. Furthermore, for it to actually happen, the incentive structure in academic mathematics would have to change drastically. Publishing papers in prestigious computer science conference proceedings explaining how you developed the basic theory of Cohen–Macauley rings and modules in a theorem prover (and of course such work would be publishable in a prestigious computer science conference proceedings – nobody has ever done it before) is perhaps not something which is recognised by promotions committees.

However there is a solution available to us right now. Formalising just the definitions and theorem statements in the Stacks Project is a much simpler task. Anybody interested in algebraic geometry would be more than welcome to learn Lean by attempting to formalise statements in Stacks Project tags. Point your web browser to the Lean Zulip instance [Zul] and ask where to get started in the #new members stream.

The reason that building such databases is important is that they will enable the community to build tools the likes of which mathematicians have never seen before. Let’s imagine that all the definitions and theorem statements in the Stacks Project have been formalised in Lean or some other theorem prover. A “hammer” is a tool which runs inside a theorem prover and which can attempt to construct mathematical arguments by piecing together results in a database. The original hammer was Isabelle/HOL’s Sledgehammer [PB10]. The cleverness behind such tools is the ability to isolate which of the many results in the database look the most useful, and to concentrate on these when attempting to prove the required result. Now consider a PhD student who is beginning to learn algebraic geometry. Such a student would then be able to ask the theorem prover a question, and the prover could attempt to use the database to answer the question positively (by piecing together a proof) or negatively (by producing a counterexample, like the website $\pi$-base [DC] is doing for counterexamples in topology). The resulting output of the computer would be able to explicitly point to references in the literature, or direct proofs of the claims it is making in its argument. This sort of tool – computer assisted learning – has the potential to beat the techniques currently used by PhD students (“google hopefully”, “page through a textbook/paper hopefully”, “ask on a maths website and then wait”, “ask another human”) hands down. But as I have stressed before, the main thing which is missing is the database of theorems, and it is up to us to construct it. The sooner it is there, the sooner the tools will appear. And the bigger the database gets, the more powerful the tools will become.

Some computer scientists have argued that mathematicians are sloppy, and our literature has errors in, and that this problem can be solved with computer proof assistants. Such an argument might initially look plausible, and I myself was a proponent of it a few years ago, but it does not stand up to much scrutiny. Firstly, the experts in our community know which results can be relied upon. Secondly, many errors are not serious and can be fixed. Thirdly, the more serious instances of this problem cannot be solved with computer proof assistants right now anyway. A great example is Mochizuki’s claimed proof of the ABC conjecture [Moc21]. This proof has now been published in a serious research journal, however it is clear that it is not accepted by the mathematical community in general. One could challenge Mochizuki, or indeed anyone, to formalise the proof in a computer theorem prover. However this would be a completely unreasonable thing to do. A computer formalisation is not expected of other proofs appearing in our literature. Furthermore, the key sticking point right now is that the unbelievers argue that more details are needed in the proof of Corollary 3.12 in the main paper, and the state of the art right now is simply that one cannot begin to formalise this corollary without access to these details in some form (for example a paper proof containing far more information about the argument).

What would however be feasible is for mathematicians to formalise parts of technical work, or to get others to do so. There might be several reasons to do such a thing – Commelin and his team have already shown that theorem provers can be used to check parts of complex proofs which humans might find it difficult to plough through, whilst learning about the mathematics in the process.

I have heard students say “I think my proof is OK” when talking about their homework. Computer proof assistants are able to tell them immediately if this is so – as long as the student has taken the trouble to learn the language of the proof assistant. Should we be teaching undergraduate mathematicians how to use computer proof assistants? I certainly think so. Patrick Massot in Orsay and myself at Imperial College London are both teaching undergraduate-level courses which do precisely this.

Students want feedback on their work as soon as possible. A computer proof assistant can supply it immediately.

Beginner students can be confused about the basics. What is the difference between $\forall\epsilon>0,\exists\delta>0,\ldots$ and $\exists\delta>0,\forall\epsilon>0,\ldots$? Once these systems become easier for mathematicians to use, students can experiment for themselves with well-chosen examples supplied by a lecturer and begin to understand what is going on. I was once told by a student “I did not understand equivalence relations, so I formalised them in Lean, and then I understood them”. Forcing students to think pedantically and logically can be good for them.

It is however worth stressing that asking a weak student to both keep up with your course and to simultaneously learn how to use a computer theorem prover is clearly asking too much from that student. The provers need to become easier to use, perhaps with graphical interfaces and documentation more appropriate for mathematicians. Asking people to change the way they teach is of course asking a lot. However, mathematics education experts will be only too happy to tell us that our preferred medium – “write for an hour on a board” – is becoming less and less appropriate for our students, who like to learn things by watching 5 minute videos or playing with interactive toys. Can we make abstract mathematics more interactive? I suspect that we can. The more people who understand how to use these machines, the sooner the new ideas will come.

I do not claim to have exhausted the possibilities here. The people who designed the CD in the 1980s surely could not envisage music services like YouTube and Spotify, or the audiobook. The people who started to think about how to make typesetting of books look good on a computer screen surely did not envisage devices like the Kindle. It is time to look beyond how we usually teach and learn mathematics, and try to understand how we as a community of mathematicians can use the inevitable digitisation of mathematical material as a tool to make our lives, and the lives of our students, better. As Carneiro once said, you can’t stop progress.