Formalising New Mathematics in Isabelle: Diagonal Ramsey

In the summer of 2017, a six week programme entitled Big Proof was held at Cambridge’s Isaac Newton Institute, “directed at the challenges of bringing proof technology into mainstream mathematical practice”. It attracted leading figures in the formalisation of mathematics, and marked the start of the present era of large formalised libraries. But some questioned whether the formalisation community’s previous achievements (such as the odd order theorem [10]) bore any useful relationship to present-day mathematics. The challenge was brand-new mathematics. And finally, we are seeing brand-new results verified prior to journal publication:

• $\mathrm{■}$

  The Liquid Tensor Experiment: an effort to verify a lemma by Scholze and Clausen in condensed mathematics. They were unsure about their large and complex proof, appealed to the research community, and the key result was formally checked within six months.

• $\mathrm{■}$

  A breakthrough in combinatorics: an exponential reduction in the upper bound for Ramsey numbers [4], announced in March 2023. A Cambridge PhD student, Bhavik Mehta, formalised this sensational result in months (see https://tinyurl.com/46d2fm3d).

Both of these were done using Lean, a proof assistant based on a dependent type theory. That raised the question of whether Isabelle, based on simple type theory, could also handle such proofs. I decided to tackle the Ramsey paper. Bhavik’s proof provided confidence that the work could be formalised, although I would work from the original article.

I should be clear at the outset about the relationship between my proof and Bhavik’s (see https://github.com/b-mehta). I have not borrowed any of the logical reasoning in Bhavik’s development: I can’t read Lean code, though I can just about decipher assertions. There are many gaps in the Ramsey paper and in my knowledge. When a lemma seemed to be missing or the authors’ meaning was unclear, I asked others for help and sometimes looked at Bhavik’s proof, which often deviated from the text. Although his formalisation was extremely helpful, I did not always follow his approach. My chief borrowings are as follows:

• $\mathrm{■}$

  the convexity argument in Lemma 4.1, discussed in §5 below (gap/error in the paper)

• $\mathrm{■}$

  an unusual Ramsey lower bound for Lemma 5.6, as discussed in §6.1 (gap in my knowledge)

• $\mathrm{■}$

  a solution to the dependence on $k$ in $F(x,y)$, as discussed in §6.7 (error in the paper)

Minor borrowings are indicated by comments in my formalisation [16].

It is easy to port a proof from one formal language to another. I have ported hundreds of thousands of lines from the HOL Light libraries. It is great to acquire these libraries, but porting an existing formalisation has little scientific interest. The point of this project is to encode a large, technically difficult mathematical work into Isabelle and observe how it went.

Isabelle and Lean are proof assistants in which types, functions and other entities can be defined and theorems proved about them. Descriptions and documentation are widely available elsewhere (e.g. for Isabelle [14] [17, §3]). The chief difference between Isabelle and Lean is that types in the latter can depend on arbitrary parameters and not merely upon other types. The advantage of Isabelle’s less expressive formalism is better automation and the avoidance of dependency issues: for example, in Lean, $i=j$ does not necessarily imply that the types $T(i)$ and $T(j)$ are the same. The Ramsey proof has nothing suggestive of dependent types, but it relies on a surprising diversity of mathematical techniques and benefits from Isabelle’s advanced automation.

The paper introduces Ramsey’s theorem (§2), then sketches the new algorithm reported in the Ramsey paper (§3). In the next three sections this algorithm is formalised (§4), one proof is explored in detail (§5) and the rest of the construction is surveyed (§6). There follows a discussion of computer algebra reasoning (§7) and conclusions (§8).

In its simplest form, Ramsey’s theorem is concerned with graphs. We imagine the edges to be coloured and are interested in monochromatic (single-coloured) complete subgraphs, or cliques. A $k$-clique is a clique of $k$ vertices; an $n$-graph is a graph of $n$ vertices.

Abbreviate $R(k,k)$ as $R(k)$, for Ramsey numbers on the diagonal. Let’s prove that $R(3)⩽6$. Since each vertex of a complete 6-graph is connected to five others, there must be at least three of the same colour, say red, from the top vertex as shown (Fig. 1). A 3-clique is a triangle, and the only way to avoid having a red triangle is to colour the dashed edges blue, creating a blue triangle. This also suggests how to colour the edges of a 5-graph, so $R(3)>5$. We know that $R(4)=18$ and $43⩽R(5)⩽46$. (The claim that $R(5)⩽46$ is new and unconfirmed [1].) Many off-diagonal values have been determined [11], such as $R(3,9)=36$. In fact, $R(4,5)=25$ has been formally verified using HOL4 [9].

This theorem can be generalised to possibly infinite hypergraphs and much else. One focus of Ramsey theory is to establish lower and upper bounds for Ramsey numbers. Already in 1935, Erdős and Szekeres found an upper bound; Erdős later proved a lower bound, giving

These bounds are far apart, and subsequent refinements over decades failed to improve the bases of the exponents. Hence the enthusiasm when Campos et al. [4] announced a proof that $R(k)⩽{(4-ϵ)}^k$, where $ϵ$ was small but positive.

There is a short proof of Ramsey’s theorem that establishes the $4^k$ bound, actually , while also motivating the new work. It involves the execution of a simple non-deterministic algorithm operating on sets of vertices $X$, $A$, $B$. First, some notation: $N_R(x)$ denotes the red neighbours of $x$ (the set of all $y$ connected to $x$ by a red edge). Similarly, $N_B(x)$ is the blue neighbours of $x$. Begin by putting all the vertices of the graph into $X$. Then, repeat the following as long as $X$ is nonempty and , :

1. 1.

   Pick an arbitrary vertex $x\in X$.

2. 2.

   If $x$ has no fewer red neighbours than blue in $X$, set $X\to N_R(x)\cap X$ and $A\to A\cup \{x\}$.

3. 3.

   Otherwise, set $X\to N_B(x)\cap X$ and $B\to B\cup \{x\}$.

Step 2 leaves in $X$ only the red neighbours of $x$. Because the same had been done for all the elements previously added to $A$, the edges between $x$ and elements of $A$ are all red, and by induction, $A$ is a red clique. Analogous remarks hold for step 3: the algorithm builds a red clique in $A$ and a blue clique in $B$. After at most $k+\mathrm{\ell }-1$ steps, we must have either a red $k$-clique or a blue $\mathrm{\ell }$-clique. Because each iteration (step 2 or step 3) removes (at most) approximately half the elements of $X$, a clique will be found if initially $|X|⩾2^{k+\mathrm{\ell }}$.

Figure 2 shows the algorithm in operation. We see the set $X$ of vertices and the arbitrarily chosen element $x$. The red expresses that all edges between $X$ and $A$ are red (as are all edges within $A$); similarly, all edges between $X$ and $B$ are blue. This property is an invariant that holds initially (because $A$ and $B$ are empty) and is preserved by steps 2 and 3.

The algorithm of Fig. 2 is unsophisticated in that the choice of $x$ is arbitrary. Campos et al. [4] get a sharper bound from a better algorithm. They break the symmetry between red and blue, adding vertices to $A$ one at a time but adding huge chunks of vertices to $B$. And they divide the vertices of the original graph into two separate sets, $X$ and $Y$.

Key to both algorithms is the notion of a book: a pair of sets $(S,T)$, where all the edges from $S\cup T$ into $S$ have the same colour (so $S$ is a monochromatic clique).

The setup for their book algorithm includes integers $k$, $\mathrm{\ell }$, with $\mathrm{\ell }⩽k$. A complete $n$-graph $G$ is coloured red/blue with no red $k$-clique or blue $\mathrm{\ell }$-clique. The algorithm manipulates the disjoint sets $X$, $Y$, $A$, $B$, where initially $A=B=\mathrm{\varnothing }$ while $X$ and $Y$ are an arbitrary partition of the vertices of $G$ into equal ($\pm 1$) parts. A further parameter is the constant $\mu \in (0,1)$. Figure 3 also shows some $x\in X$ being chosen on the basis of the density of red edges linking its neighbours with $Y$. (The density of edges between $X$ and $Y$ equals the number of such edges divided by $|X||Y|$.)

The process runs until either $|X|⩽R(k,\lceil {\mathrm{\ell }}^{3/4}\rceil )$ or $p⩽1/k$, where $p$ denotes the density of red edges between $X$ and $Y$. Here is a sketch of the possible execution steps:

• $\mathrm{■}$

  Degree regularisation involves removing from $X$ all vertices having “relatively few” red neighbours in $Y$. This is performed at every even-numbered execution step.

• $\mathrm{■}$

  An odd-numbered step is taken as follows:

  • –

    A big blue step, if there exist $R(k,\lceil {\mathrm{\ell }}^{2/3}\rceil )$ vertices $x\in X$ such that

    $$|N_B(x)\cap X|⩾\mu |X|,$$

    then a “large” blue book $(S,T)$ is chosen and the sets updated by

    $$X\to T,Y\to Y,A\to A,B\to B\cup S.$$

  • –

    But if not, then a central vertex $x\in X$ exists satisfying $|N_B(x)\cap X|⩽\mu |X|$ and a second technical condition. If the density of red edges between $N_R(x)\cap X$ and $N_R(x)\cap Y$ is sufficiently high, a red step is performed:

    $$X\to N_R(x)\cap X,Y\to N_R(x)\cap Y,A\to A\cup \{x\},B\to B.$$

    Otherwise, as in the previous algorithm, $x$ is moved to $B$, in a density-boost step:

    $$X\to N_B(x)\cap X,Y\to N_R(x)\cap Y,A\to A,B\to B\cup \{x\}.$$

The paper [4] presents further definitions specifying aspects of execution traces. Its next 20 or so pages are devoted to proving that big blue steps really are big, density-boost steps really boost the density of red edges between $X$ and $Y$, and providing lower bounds for $Y$ and $X$ as execution proceeds; the point is to show that they do not decrease too quickly as a function of execution steps of various kinds. Next comes the so-called zigzag lemma, which bounds the number of density-boost steps (which decrease both $X$ and $Y$). It emerges through their work that one of the termination conditions, $p⩽1/k$, can never happen: the red density remains high enough.

The authors need a further 10 pages to obtain the headline result. Here they typically take a candidate Ramsey number, construct an execution of the algorithm by defining $X$, $Y$ and so forth, and use the lemmas proved previously to deduce their claims. The authors first find exponentially improved bounds for $R(k,\mathrm{\ell })$ when $\mathrm{\ell }⩽k/9$ (“far from the diagonal”), then when $\mathrm{\ell }⩽k/4$ (“closer to the diagonal”) and finally for $\mathrm{\ell }=k$.

The proofs rely on a variety of elementary techniques for estimating real numbers, as well as asymptotic reasoning and finding upper/lower bounds for real functions. The probabilistic method pioneered by Erdős is used twice. The Isabelle formalisation [16] of the paper comprises some 11,000 lines (for the Lean one, 13,870 lines). A further 1500 lines were devoted to formalising background mathematics. The proofs are too long, difficult and intricate to present in full, but let’s look at a few representative examples.

The diagonal paper can be seen as an abstract example of program verification. The book algorithm is indexed by a simple step counter and operates on its four-component state. The state variables at step $i$ are written $X_i$, $Y_i$, $A_i$, $B_i$, with $i=0$ denoting the initial state.

A succession of properties about the state are proved in terms of measures of the execution itself, primarily the numbers of steps of the various kinds. The authors assign $ℛ$, $ℬ$, $𝒮$ and $𝒟$ to the sets of indices, corresponding to an execution of a red step, a big blue step, a density-boost step and a degree regularisation step respectively, and they write $t=|ℛ|$ and $s=|𝒮|$ for the number of red steps and density-boost steps in a full execution. I found it convenient to introduce also $|\mathscr{H}|$ for the set of indices after the algorithm effectively halts.

The paper is concerned with the book algorithm’s execution state but also its context: a graph of $n$ vertices, the edges coloured red/blue and many other details. We don’t want to repeat this boilerplate in every lemma statement. Luckily, Isabelle’s locale mechanism [2] lets us declare these parameters and their constraints in one place, along with associated proofs and even dedicated syntax. A locale encapsulates a local scope, but internally it is simply a predicate.

The locale declarations for the diagonal Ramsey development give an idea what we are dealing with. For starters, although it only becomes evident much later, one parameter of the construction is $p_0\in (0,1)$: the minimum density of red edges between $X_0$ and $Y_0$.

Locales can be combined flexibly to build more complicated structures. Here we combine a formalisation of finite simple graphs [6] with the previous locale, adding the assumptions that our graph is complete and the requirement that the underlying type is infinite.

We further extend it with a colouring that has no red $k$-cliques or blue $\mathrm{\ell }$-cliques.

We need two separate locales for the book algorithm itself. In the preliminary proofs (sections 4–8 of the diagonal paper), it is governed by a given fixed $\mu \in (0,1)$:

In the final proofs (sections 9–11), the parameter is called $\gamma$ and is defined by $\gamma =\frac{\mathrm{\ell }}{k+\mathrm{\ell }}$:

Much of the formalisation takes place within locale Book, with the parameters specified above immediately accessible. Towards the end, while proving the headline claims, we start outside the locale. Then we create a graph, colour its edges, choose $X_0$ and $Y_0$, thereby creating an instance of Book. These steps correspond to the authors’ remark “we now apply the book algorithm”.

Here is a glimpse at the algorithm itself. Recall that an odd-numbered step can be a big blue step, a red step or a density-boost step.

The execution stepper itself must also take care of the even-numbered steps (degree regularisation) and the termination condition (when it leaves the next state unchanged):

Functions like many_bluish and choose_blue_book refer to details of the algorithm omitted here. Many other definitions and basic lemmas are also omitted.

The first substantial proof is Lemma 4.1, stated by the authors as follows [4, p. 11]:

Here $X$ is any set, not necessarily a state component of the book algorithm, though that’s how the lemma will be applied. The proof is under a page, but it presents many complications. For starters, some trivia: it is already assumed that there are no red $k$-cliques in the given graph, so we can already rule out the possibility of such a clique in $X$. And by convention, expressions like $R(k,{\mathrm{\ell }}^{2/3})$ don’t indicate whether the floor or the ceiling of ${\mathrm{\ell }}^{2/3}$ is intended. The omission looks strange to me; in most cases, I have assumed the ceiling.

A more serious omission is that the theorem only holds for sufficiently large $\mathrm{\ell }$ and all $k⩾\mathrm{\ell }$. This $\mathrm{\ell }$ may depend upon $\mu$ alone; moreover, it must be constant as $\mu$ ranges over a closed subinterval of $(0,1)$. The need for this becomes apparent only 19 pages later, in Lemma 9.3. Constraints on $\mathrm{\ell }$ (or, more usually, $k$) need to be picked up here and there in the proof. It is quite common that a claimed inequality does not hold in general, but only for sufficiently large $k$.

So we need to decide how to formalise the “sufficiently large” condition. The elegant approach uses the eventually topological filter [13], which is available in both Isabelle/HOL and Lean. Initially, I followed Bhavik and used eventually, making the various constraints local to each proof and thus hidden. I later adopted the approach of making these constraints explicit: to define a bigness predicate for each theorem, justifying each predicate by proving a lemma (expressed using eventually) to check that the predicate indeed holds for all sufficiently large $\mathrm{\ell }$. This seemed more natural, while also retaining access to the specific conditions used. Eventually it allowed $k$, $\mathrm{\ell }$, $\mu$ and their constraints to be migrated from the theorem statements to the Book locale, to be written only once rather than many times.

The bigness predicate Big_Blue_4_1, for Lemma 4.1, is a conjunction of six inequalities, such as $l⩾{(6/\mu )}^{12/5}$. Recall that the property may depend upon $\mu$ alone and the obtained $\mathrm{\ell }$ must be good over a closed interval. The corresponding bigness lemma refers to the closed interval $[{\mu }_0,{\mu }_1]$, where . Here there is no need to assume , so the precondition could be simplified to $\mu ⩾{\mu }_0$. Uniformity in the lemma statements will be convenient however, since there will be lots of them. The proof, some 40-odd lines, is routine and deals with the six inequalities separately.

Here is the formal statement of Lemma 4.1. It’s easy to state, because the most technical parts of the theorem statement (many_bluish and good_blue_book) have already been formalised for the specification of the book algorithm.

Before proving this, it was necessary to build a basic library of Ramsey numbers, including the Erdős lower bound $2^{k/2}⩽R(k,k)$ by the famous probabilistic argument. The formal proof of Lemma 4.1 is some 350 lines; let’s look at some of the details.

Early in the proof we obtain a blue $m$-clique, $U\subseteq X$, where $m={\mathrm{\ell }}^{2/3}$. The text continues:

Let $\sigma$ be the density of blue edges between $U$ and $X\setminus U$, and observe that

$$\sigma =\frac{e_B(U,X\setminus U)}{|U|\cdot |X\setminus U|}⩾\frac{\mu |X|-|U|}{|X|-|U|}⩾\mu -\frac{1}{k}.$$

The first equality holds by definition, but the two subsequent inequalities require heavy manipulations of sums: more than 70 proof lines even to yield the weaker claim $\sigma ⩾\mu -2/k$. (The weakening, a hint from Bhavik, does no harm: eventually we’ll need $2{\mathrm{\ell }}^{-5/12}⩽\mu -2/k$, which holds for large enough $\mathrm{\ell }$. It simply becomes part of the bigness predicate.) The first inequality follows by careful counting of edges, while the second relies on $|X|⩾R(k,m)$ and properties of Ramsey numbers. This painful example gives a good impression of how dense the presentation is throughout the diagonal paper. The proof continues:

Let $S\subset U$ be a uniformly-chosen random subset of size $b$, and let $Z=|N_B(S)\cap (X\setminus U)|$ be the number of common blue neighbours of $S$ in $X\setminus U$. By convexity, we have

$$𝔼[Z]={\left(\genfrac{}{}{0pt}{}{m}{b}\right)}^{-1}\sum _{v\in X\setminus U}\left(\genfrac{}{}{0pt}{}{|N_B(v)\cap U|}{b}\right)⩾{\left(\genfrac{}{}{0pt}{}{m}{b}\right)}^{-1}\left(\genfrac{}{}{0pt}{}{\sigma m}{b}\right)\cdot |X\setminus U|.$$

The first equality requires a probabilistic argument. The expectation of $Z(S)$ for the randomly chosen subset $S$ can be formalised by setting up a probability space [8]. “Convexity” is doing a lot in the inequality. The function $f$ is said to be convex if $f\left({\sum }_{i\in S}{a}_i{y}_i\right)⩽{\sum }_{i\in S}{a}_{i}f(y_i))$ where $S$ is nonempty and finite, $a_i⩾0$ for $i\in S$ and the $a_i$ sum to 1. In our proof, each $a_i={|X\setminus U|}^{-1}$ and the convex function is the real-valued generalised binomial $\lambda x.\left(\genfrac{}{}{0pt}{}{x}{b}\right)$, which unfortunately is not actually convex. I adopted Bhavik’s elaborate fix for this problem, which was to define an alternative real-valued binomial that was convex and agreed with the original where it mattered, on the integers.

The proof continues:

Now, by Fact 4.2, and recalling (10), and that $b={\mathrm{\ell }}^{1/4}$ and $m={\mathrm{\ell }}^{2/3}$, it follows that

$$𝔼[Z]⩾{\sigma }^b\exp \left(-\frac{b^2}{\sigma m}\right)\cdot |X\setminus U|⩾\frac{{\mu }^b}{2}\cdot |X|,$$

and hence there exists a blue clique $S\subset U$ of size b with at least this many common blue neighbours in $X\setminus U$, as required. $\mathrm{\square }$

Several dozen detailed and tedious lines of inequality calculations take care of the probability and counting arguments making up this final part. Lemma 4.1 is among the trickier theorems but its proof is typical of the sort of reasoning used throughout the paper: estimation and calculations involving edge density, edges and vertices. On the other hand, the paper has only one further probabilistic argument: to derive a non-standard lower bound for Ramsey numbers.

It isn’t possible to go through any other proofs in such detail, but let’s have a glimpse at the key milestones. To begin, let’s establish some conventions. Recall that the book algorithm operates on state variables $X$, $Y$, $A$ and $B$. Some other variables are defined in terms of them, notably $p_i$, the density of red edges between $X_i$ and $Y_i$.

We have an issue with the subscripts: the Isabelle and Lean formalisations both write $X_i$ for the value of $X$ after $i$ execution steps, when Campos et al. [4] write $X_{i-1}$. Complicating matters further, everyone agrees to write $x_i$ for the value of the “central vertex” after $i$ execution steps.

In Isabelle, $X_i$ is written Xseq i and similarly for $Y$, $A$, $B$ and $p_i$ . Note that $ϵ=k^{-1/4}$, so $ϵ$ depends on $k$: it is formalised as eps k but within locales where $k$ is available (No_Cliques and beyond) it’s abbreviated to simply $\mathrm{\epsilon }$. Some theorems refer to the situation after the algorithm halts; the step number at which it halts is written halted_point.

During the 1990s, researchers sought to combine the capabilities of computer algebra systems (such as Maple and Mathematica) with interactive theorem provers. Computer algebra systems could deliver wrong answers, due to overly aggressive simplification or outright bugs. A student of mine, Clemens Ballarin, worked on this problem [3]. A difficulty was finding an application, since most computer algebra users are not performing proofs. But the diagonal Ramsey proof needs computer algebra everywhere: derivatives (typically for identifying maxima), limits, continuity, Landau symbols, high precision exact real arithmetic. We are frequently forced to perform precise numerical calculations or to prove the existence of a large enough $\mathrm{\ell }$ satisfying some complicated condition.

Isabelle/HOL provides a number of automatic tools to carry out such tasks:

• $\mathrm{■}$

  Eberl’s real_asymp proof method [5], to prove theorems about limits and Landau symbols for real-valued functions

• $\mathrm{■}$

  Hölzl’s approximation method [12], to do exact real calculations using interval arithmetic

• $\mathrm{■}$

  the rule set derivative_eq_intros, useful for performing symbolic differentiation

The last item needs further explanation, because it is not packaged as a neat proof method. Taking the symbolic derivative of a function by repeatedly applying syntactic rules is an easy programming exercise dating back nearly 60 years [18]. Theorems stating the rules for differentiating functions such as multiplication, division, sine or cosine, packaged in the identifier derivative_eq_intros, can take derivatives of quite large expressions when interleaved with calls to the simplifier.

Here is an example, from Lemma 9.3, proving that the function $1-1/200x$ is concave on $[1/10,1/5]$ by calculating its second derivative and noting that $-1/(100x^3)\le 0$ if $x\in (0,1)$.

The diagonal Ramsey formal development includes 16 symbolic differentiations, 30 calls to approximation and 60 calls to real_asymp. Many of these would be difficult to establish without those tools. Let’s look at the formal proof that

This is the $o(k)$ function mentioned in Lemma 7.2, which we saw in §6.3 above. The formal proof requires merely unfolding the definition, then calling real_asymp. (The complexity class $o(k)$ is formalised as o(real), where real is the injection from $\mathbb{N}$ into $ℝ$.)

Many of the asymptotic lemmas claim that some property $P(\mu ,\mathrm{\ell })$ holds for all sufficiently large $\mathrm{\ell }$ and all $\mu$ ranging over some closed subinterval $[{\mu }_0,{\mu }_1]\subset (0,1)$. The real_asymp method does not work for intervals, but monotonicity helps: if $P(\mu ,\mathrm{\ell })$ is preserved as $\mu$ increases, then it is enough to check $P({\mu }_0)$, and if it is preserved as $\mu$ decreases, it is enough to check $P({\mu }_1)$. And one or the other held every time.

The calls to approximation come in two forms. Most are simple calculations, such as $835.81⩽3\cdot {\log }_2(5/3)/5\cdot {\log }_{2}2727$, which requires high precision. However, the proof of Lemma 12.3, mentioned above, twice requires reasoning over a closed interval.

The splitting keyword controls the interval splitting in the search. The claim proved is

   log 2 (5/2) + (3 * y / 5 + 5454 / 10ˆ4) * log 2 (5/3) +
   y * log 2 (2 * (3 * y / 5 + 5454 / 10ˆ4 + y) / (5 * y))  $⩽$  2 - 1/2ˆ11

The two approximation calls with splitting use 27 seconds of CPU time in total. In comparison, the entire diagonal Ramsey proof (including those calls) takes 218 seconds on an M2 MacBook Pro.

This project was a huge amount of work: 251 days, just over eight months. Its de Bruijn index (the ratio between the formal and informal text, after compression) is relatively high, at 5.6, a sign of the work’s difficulty. (Common is 4 [7].) Here is the proof of the main theorem, which includes limit reasoning using filters and a call to approximation.

A particular advantage of Isabelle is that proofs, even really big ones, are easy to modify. The structured proof language localises the points at which proofs fail, and the strong automation can often correct those failures with a mouse click. My many mistakes sometimes required fundamental changes, which could be pushed through easily enough. Once the first version of the proof was done, I noticed that $k$, $\mathrm{\ell }$, $\mu$ and their associated constraints could be moved into the locales (as opposed to being explicit arguments throughout), yielding a transformative improvement in readability.

Bhavik’s Lean proof is slightly longer. He adopted a different fix to the errors in theorems 9.1 and 10.1 and to the issues in sections 11 and 12. Lacking the approximation and real_asymp tools, he obtained the required results manually. The splitting example above cost him “over 200 lines of analytic arguments, and at least 150 lines of interval arithmetic calculations” (private communication). Because he used filters rather than bigness predicates, a lot of context had to be repeated many times. Given all that, his proof is admirably concise.

What do we learn from this project? Mainly, it provides more evidence that proof assistants – including Isabelle/HOL – can cope with serious new mathematics. Although the techniques in the paper hardly go beyond the undergraduate level, it is an intricate construction combining probability, graph theory, asymptotics and high precision numerical calculations. It is the sort of proof that would surely attract doubters, but with two largely independent formalisations, in different systems, there can be little room for doubt anymore.

With so much mathematics formalised, both in both Lean and in Isabelle [15], it’s reasonable to say that the point has been made. But still: so-called proof assistants should actually be assisting mathematicians in their work, as they already assist computer scientists. One line of attack would begin with the Isabelle proof just finished. The diagonal paper is full of seemingly arbitrary numerical choices. The Isabelle proof is a living document that you can tinker with, making a change and immediately seeing what goes wrong. Somebody who knows what they are doing could surely find a sharper bound or a simpler proof.