The machine that only knows the rules
A proof assistant is not an automated mathematician. It is a piece of software that holds a mathematical development in memory and refuses to accept any step that does not follow from a fixed, small set of inference rules. The mathematician writes definitions and proof scripts; the system elaborates them into terms of a formal language; a component called the kernel decides whether those terms are well typed, which in these foundations is the same question as whether the proof is valid. Everything else in the system — the tactic language, the search procedures, the editor integration, the libraries — is untrusted convenience. If any of it is buggy, the worst outcome is that the kernel rejects your work.
That architecture is the whole trick, and it is deliberately old. It descends from the LCF tradition, in which theorems are values of an abstract type that can only be constructed by calling the primitive rules. The engineering consequence is that the amount of code you have to believe stays roughly constant while the amount of mathematics on top of it grows without limit. Barendregt and Wiedijk state the design goal as a criterion, named for N. G. de Bruijn: an implementation satisfies it when proof generation and proof checking are independent, so that the low-level logical proof is stored in full and a small verifying program can check a proof of many megabytes by confirming only that a handful of logical rules were always observed [5].
Gonthier’s account of the Four Colour Theorem formalisation shows what that buys in practice. His Coq development can emit a proof witness — a term in a higher-order lambda calculus recording the chain of formal logical steps. Because the witness records only logical steps and not the computation steps needed to produce them, its size stays reasonable even when the underlying proof involves enormous calculation, and it can in principle be checked by an independent program [1]. The point is not that machines are infallible. It is that the object to be trusted has been made small enough for a person to audit, and small enough that a second, unrelated implementation can be written to check it.
The trust base moves; it does not vanish
Nothing about this makes the residual trust base zero, and the careful practitioners say so first. Gonthier lists his own: the correctness of the formal proof still depends on the processor, the operating system, the Coq checker and the OCaml compiler that built it. His argument is not that these are beyond doubt but that none of them is specific to the Four Colour Theorem. They are off-the-shelf, general-purpose, and exercised on innumerable other jobs — probably, he suggests, more thoroughly than the mind of any individual mathematician reviewing a manuscript could ever be [1].
The second component is axiomatic. A proof assistant proves theorems in a particular foundation, and that foundation has commitments. Coq is built on intuitionistic type theory, and the Four Colour development had to choose a form of the supremum axiom for the reals that implies excluded middle [1]. Lean’s library extends the calculus of inductive constructions with quotient types and two axioms — a choice principle and propositional extensionality — and mathlib is explicitly and unapologetically classical [6]. These are not hidden, but they are assumptions, and a reader who wants to know exactly what was proved has to know which ones are in force.
The third component is cross-checking, which the field does perform. As part of a systematic audit of the Kepler formalisation, Mark Adams exported the main part of the verification to the independent HOL Zero system and reconfirmed the result [4]. That is the de Bruijn criterion cashed out: a proof produced under one implementation, re-checked under another written by someone else.
The fourth component is the one that actually breaks, and it is not a kernel bug. It is the statement.
Where formalisation settled an argument
The Four Colour Theorem is the canonical case because the dispute is documented. Appel and Haken proved it in 1976 by using computer programs to carry out a case analysis covering, as Gonthier puts it, quite literally a billion cases. The criticism was of two kinds. One was aesthetic: a simple statement was expected to have a proof that explained, at least informally, why the theorem is true, rather than opaque IBM 370 assembly language programs. The other was, in Gonthier’s own words, “more rational scepticism” — computer programming is error-prone and hard to relate precisely to the formal statement of a theorem, and the proof also involved an initial manual case analysis of some ten thousand cases, difficult to verify, in which several small errors were in fact detected [1].
Robertson, Sanders, Seymour and Thomas published a streamlined proof in 1995 using C programs to check both the giant and the large case analyses, which cleared up most doubts about the truth of the theorem. Gonthier’s formalisation, completed with Benjamin Werner and fully checked by Coq, closed the remaining gap by removing what he identifies as the two weakest links: the manual verification of the combinatorial arguments, and the manual verification that custom programs correctly filled in parts of those arguments. A single formal script covered both the mathematical and the computational halves [1].
The Kepler conjecture is the sharper case, because there the social machinery of refereeing visibly failed. Hales and Ferguson announced a solution in 1998. A panel of twelve referees was assigned. The review dragged on for years until, in Hales’s account, the referees became exhausted and quit; full publication did not occur until nearly eight years after submission, and the editors of the Annals of Mathematics issued a policy on computer-assisted proofs avowing that the computer part may not be checked line by line but will be examined for the methods by which the authors eliminated or minimised possible sources of error [4]. Hales is explicit that the formalisation project was launched out of frustration at that delay, as a way to bypass the referees. It also arrived in a field that had already been poisoned once: around 1990 a claimed proof by Wu-Yi Hsiang had to be rebutted with explicit counterexamples, and Hales writes that for a few years the research area became toxic [4].
The formal proof was completed by a large collaboration in 2014 and published in 2017, in a combination of HOL Light and Isabelle [3]. The scale is worth stating precisely: about half a million lines of proof script, an estimated twenty work years, a main verification that runs in roughly five hours on a laptop, and a nonlinear-inequality verification requiring about five thousand CPU hours in a cloud computation [4]. What was demonstrated was not that the 1998 proof had been wrong. It was that a proof whose referees could not finish could nonetheless be settled — and that the settling was reproducible by machine in an afternoon.
The Odd Order Theorem sits differently again. Gonthier and a large team formalised the Feit–Thompson theorem in Coq over a six-year collaborative effort, producing a proof that is constructive and relies on nothing but the axioms and rules of Coq’s foundational framework [2]. Nobody doubted Feit–Thompson. What that project demonstrated was capacity: that a long, entirely human, classical text — hundreds of pages of finite group theory — could be brought inside a formal system, and that doing so forces the construction of reusable libraries in finite group theory, linear algebra, Galois theory, and the theories of real and complex algebraic numbers.
A formal proof of the wrong statement is worthless
Here is the failure mode that no kernel can catch. The kernel certifies that a term inhabits a type. It has no view on whether that type is the theorem you meant. If the formal statement quietly says something weaker, or ranges over the wrong objects, or has a hypothesis that is vacuously satisfiable, the machine will happily certify it and the result will be worth nothing.
Practitioners treat this as the real audit surface, and they design for it. Gonthier’s argument is that the fully formal statement is short enough to read: the definitions of a simple planar map, region and adjacency take about thirty lines of his development, and together with the formal definition of the real numbers — about two hundred lines in total — those are all one needs to read and understand in order to be satisfied that the theorem in the development is indeed the Four Colour Theorem. The other sixty thousand or so lines, he writes, can be read for insight or even entertainment, but need not be reviewed for correctness; that is the machine’s job [1]. The audit does not disappear. It concentrates.
Hales made the same move on the Kepler conjecture and describes the choices involved. The formal statement was deliberately engineered for readability: all mention of measure was removed, and the theorem was formulated as a claim about finite packings inside a large ball, which introduces a boundary error term but avoids importing measure theory into the statement. Cleaned up, it reads:
Every symbol here is an invitation to a fidelity question. What does packing unfold to? Is the error term doing more work than it appears? Hales notes that the constant is not explicit in the statement, and that the theorem includes no uniqueness claim [4]. None of this is concealed — but none of it is checked by the kernel either.
Maintaining correspondence between the informal text and the formal scripts was itself a project. The Flyspeck team gave each lemma a randomly generated seven-letter tracking code appearing in both the LaTeX source and the HOL Light script, so that lemmas could be tracked across versions as both texts were edited. Hales observes that keeping an informal and a formal text side by side violates the software engineering principle of Don’t Repeat Yourself, and that considerable effort was required to maintain alignment across edits [4].
And then there is the admission that ought to be quoted whenever anyone describes a formal proof as absolute. In Flyspeck, the classification of tame planar graphs was proved in Isabelle by Nipkow, Bauer and Schultz, while the rest lives in HOL Light. The two were never linked mechanically: the statement of the classification theorem is translated by hand from Isabelle into HOL Light, where it is accepted as an unproved postulate. “This hand translation,” Hales writes, “is the weakest link in the entire Flyspeck project” [4]. A formal proof, in other words, whose most delicate joint is a human retyping a sentence between two languages.
The related lesson concerns verifying code that was never written to be verified. The Isabelle definition of a planar graph is effectively a black box: graphs are whatever an edge-adding algorithm produces, an algorithm Hales originally implemented in Mathematica and later Java in 1993, with no thought of formalisation. He calls verifying a HOL Light translation of an Isabelle translation of an ML translation of that old Java program a very unpleasant experience, and states the rule it violates: never verify code that has not been written with verification in mind [4].
The bottleneck is the library
The popular picture of formalisation has the computer searching for a proof. The practitioners’ picture has a human hunting for a lemma that may not exist yet. Hales recorded about ten thousand searches of his own during Flyspeck, because in these systems each theorem has a name and, with few exceptions, every invocation requires citing it by name [4]. Formalisation is limited less by inference than by inventory.
That inventory is a serious engineering artefact. The mathlib paper reports growth from fifteen thousand to a hundred and forty thousand lines of code in the two years after Lean’s core library was split out, reaching 140,085 lines and 34,168 declarations by December 2019, contributed by 73 people and managed by a team of 11 maintainers [6]. Those maintainers exist because a shared library is not a pile of results; it is a set of interlocking definitional choices — how a topological space is presented, how an algebraic hierarchy is layered — and a bad choice propagates.
Flyspeck illustrates the cost of optimising locally instead. Most of its lemmas were formulated minimally rather than in generality, because the goal was the Kepler conjecture rather than library development; the formalisation avoids matrices, avoids integration on manifolds, and uses only a special case of the Jordan curve theorem [4]. The bill arrives later. After the project finished, Harrison converted limits in his analysis library from nets to filters to bring HOL Light in line with other assistants, and the proof scripts had to be updated. At one point the collaboration was grappling with three different libraries for lists, with subtle differences between them, because pieces had arrived from Isabelle, from Coq and from HOL Light natively [4].
The contrast with a well-stocked library is stark. Buzzard’s account of the Liquid Tensor Experiment credits Scott Morrison’s six years of category theory development inside mathlib with providing a stable foundation to build on [9]. That is the actual shape of the field: a decade of unglamorous definitional infrastructure is what makes a headline formalisation possible, and the headline formalisation is what gets reported.
Formalisation changed how the work is organised
The social change is not incidental; it may be the most consequential part. Hales puts the mechanism plainly: in a formalisation project, the definitions and statements of lemmas act as a specification, the top-level architecture shows how the main theorem follows from the lemmas, and any formal proof of a lemma — no matter where, how, or by whom it is produced — advances the project [4]. That is a different collaboration model from a conventional multi-author paper. Contributions are separable, verifiable on arrival, and do not require the contributor to hold the whole argument in mind.
The Liquid Tensor Experiment is the clearest demonstration. In December 2020 Peter Scholze publicly challenged the formalisation community to verify a theorem of his with Dustin Clausen; the project was completed on 14 July 2022, after roughly eighteen months, led by Johan Commelin with more than twenty contributors and substantial work by Adam Topaz on homological algebra and condensed mathematics [8]. The internal proportions are instructive: about thirty thousand lines of Lean for the five-page proof of one theorem, and about sixty thousand lines for the five lines connecting it to the result actually wanted — one month to formalise the statement, five more for its proof, and a year for those five lines [9].
Scholze’s own reason for asking is worth quoting because it is not about doubting the kernel. He said he was essentially unable to keep all the objects in his head at once, and that he had been “sweating a little bit” over a subtlety about quotient norms — that an infimum need not be a minimum — which, he judged, would likely have been overlooked in an informal verification [7].
The tooling has since made the pattern routine. Patrick Massot’s blueprint system links a human-readable proof outline to the Lean formalisation and generates a dependency graph, so contributors can see which nodes are open and work asynchronously without waiting for prerequisites. Terence Tao used it in November 2023 to organise the formalisation of the polynomial Freiman–Ruzsa conjecture with Yael Dillies and Bhavik Mehta, coordinating over the Lean Zulip and accepting contributions as pull requests; the dependency graph was completed in about three weeks [10]. Tao reports that the exercise turned up one minor omission in the original write-up concerning group properties, causing no mathematical damage — and, notably, argues that for large existing bodies of work the practical approach is strategic partial formalisation, formalising the key calculations while accepting cited results as black boxes [10].
Hales draws a distinction that captures the cultural split inside this practice: formalisers divide into scribes, who take their duty to be a faithful copy of the original text, and revisionists, who overhaul the proof to achieve something better. He counts himself a revisionist — the Kepler proof was completely transformed during formalisation, and week by week he found that revising the mathematics advanced the project more than formalising what already existed [4].
Automation, without the gloss
Two distinct technologies get conflated in coverage, and they deserve separating.
The first is the hammer: a tool that takes the current goal, selects relevant facts from a large library, translates the goal and those facts into the logic of external automatic theorem provers, runs them, and then reconstructs the discovered proof inside the assistant’s own kernel so that nothing unverified is trusted. The survey by Blanchette, Kaliszyk, Paulson and Urban describes exactly these ingredients — provers that cope with hundreds of axioms, sound translations, heuristic and learning-based methods for selecting relevant facts from large libraries, and reconstruction inside the proof assistant [11]. Premise selection is where machine learning entered this field, and it entered as a relevance filter over a library, not as a substitute for one.
The second is neural proof search. LeanDojo instruments Lean so that models can interact with the proof environment programmatically, and provides fine-grained annotations of which premises were used where; its ReProver model uses that program analysis to identify accessible premises and hard negative examples for retrieval. The reported result is that retrieval-augmented proving outperforms non-retrieval baselines and GPT-4 on a benchmark of 98,734 theorems, trained with about one GPU week [12]. That is a real result and a modest one, and the paper frames premise selection as the bottleneck — which is the same diagnosis the human formalisers give.
Vendor claims should be labelled as such. Google DeepMind stated in July 2024 that AlphaProof and AlphaGeometry 2 together scored 28 of 42 points on the 2024 International Mathematical Olympiad, one point below the gold threshold. The same post records the caveats: the problems were manually translated into formal language, two combinatorics problems went unsolved, one problem was solved within minutes while others took up to three days, and human contestants work under a 4.5-hour session limit [16]. Those are the company’s own qualifications, and they matter — a system given three days on a hand-formalised statement is not competing under the conditions the medal describes.
Prediction, with its conditions stated. Over the next three years, to mid-2029, I expect the dominant published use of learned models in formalisation to remain lemma retrieval and single-step tactic suggestion inside human-directed projects, rather than end-to-end proof of research-level theorems from informal statements. The assumptions are that library growth continues to be the limiting input, that autoformalisation of research statements remains unreliable enough to require human authorship of the statement, and that no change in funding removes the maintainer capacity that keeps libraries coherent. Observable indicators: the share of merged mathlib contributions whose statements were authored by a model; whether blueprint-style projects begin listing model-generated lemmas as leaf nodes closed without human editing; and whether any previously open problem is resolved by a machine-produced formal proof whose statement a human did not write. The disconfirming condition is straightforward: a research-level theorem, not previously proved informally, formalised and proved end-to-end from an informal problem statement with the formal statement itself machine-generated and accepted without human revision. If that happens before mid-2029, this prediction is wrong.
Correctness, understanding, and an unresolved argument
The disagreement here is genuine, and it is not between believers and Luddites. It is about what a proof is for.
Thurston’s position, stated long before the modern tools, is that mathematics advances through forms of progress not captured by formal proofs of theorems; that what mathematicians actually produce and consume is understanding, and that a correct derivation is not the same object as an explanation [14]. Weatherall and Wolfson push this to an explicit challenge, arguing that formal correctness is neither necessary nor sufficient for a proof to have epistemic value, and inverting the usual dependency: formal correctness tracks mathematical correctness because it was designed to do precisely that, so formal logic is best read as a mathematical theory describing mathematical practice rather than as a standard imposed on it. If mathematics moved beyond what current formal systems capture, on their account, logicians would build new systems rather than mathematicians change their work [15].
Against that stands testimony from inside the projects. Scholze’s report of the Liquid Tensor Experiment is not a report about certainty. He writes that he did not understand why the argument worked, or why one had to move from the reals to a certain ring of arithmetic Laurent series, and that during the formalisation he realised the key move was a reduction from a non-convex problem over the reals to a convex problem over the integers [7]. That is understanding acquired through formalisation, and it is a data point the sceptical position has to accommodate. Buzzard’s claim from the same episode is narrower and organisational: that a group of mathematicians focused on formalising an arbitrary piece of modern mathematics can get it done, however complex the theory [9]. Avigad’s framing is the most ecumenical — that formal systems now make it possible to encode mathematical knowledge in digital form, and that the interesting question is enumerating the specific ways this helps mathematicians do mathematics, rather than adjudicating whether it replaces anything [13].
I do not think the evidence currently settles this. Both sides are describing real phenomena. Formalisation demonstrably produced understanding in at least one celebrated case, and it demonstrably produces long stretches of tedium that illuminate nothing — the sixty thousand lines Gonthier says need not be read for correctness are not an explanation of anything. Hales’s scribe-versus-revisionist split maps onto the dispute neatly: a scribal formalisation is a certificate and makes no claim to explain, whereas a revisionist formalisation, by forcing every definition into a form that composes, sometimes yields a better proof than the one it started from.
What is not in dispute is narrower and more solid. A proof assistant relocates trust from an unbounded manuscript to a bounded kernel, a stated list of axioms, and a formal statement short enough to read. It settled two arguments that human refereeing could not — one about a billion machine-checked cases, one about a manuscript twelve referees could not finish. It changed collaboration by turning a proof into a specification against which strangers can contribute checkable pieces. And it has made the weak point of a proof legible: not the reasoning, which the machine now guarantees, but the sentence at the top, which it never will.
