Verification abundance, adjudication scarcity: what happens to mathematical knowledge when proof checking becomes free

In May 2026 an OpenAI model produced a counterexample to the Erdős unit distance conjecture. Five mathematicians published a digested, human verified version of the argument the same day, and the result was absorbed into the literature within weeks. In August 2026 the same laboratory published ten results in mathematics and theoretical computer science, each accompanied by a machine checkable Lean 4 certificate with no unproved steps. Four weeks later, one of those results is the subject of an unresolved dispute in which the mathematical community has been unable to determine whether the formalization means what it claims to mean. We argue that the difference between these outcomes is structural rather than accidental, and that it follows from an inversion that abundant machine checking produces. We distinguish three layers of verification: derivational validity, which a kernel checks; representational fidelity, whether the formal statement means the informal question; and epistemic significance. Only the first is mechanizable, and we give the reason, inherited from Fetzer, why the second is not mechanizable even in principle. Driving the first to zero cost does not reduce the verification burden on a body of knowledge; it transfers that burden onto layers whose throughput is fixed by the supply of qualified readers. We support this with measurements of the published artefacts. In the August corpus the kernel checked proofs total 20.6 MB while the statements requiring human audit total 55.6 KB, a ratio of 379 to 1, and those statements introduce 218 bespoke definitions rather than relying on the community vetted library. The audit surface is therefore small but irreducibly expert. We conclude that engineering can shrink the audit surface and cannot manufacture the auditor, and that the resulting scarcity is not of verification but of adjudication. We offer a six category taxonomy of representational mismatch usable as an audit protocol, a disclosure schema for machine generated discovery claims, and an analysis of what transfers to software, cryptography and regulated decision systems.

Introduction. 1 Two results, two fates On 20 May 2026 OpenAI announced that a general purpose reasoning model had disproved the Erdős unit distance conjecture, a problem posed in 1946 concerning the maximum number of pairs of points at distance exactly one among n points in the plane (OpenAI 2026a). The prevailing expectation was that rescaled grid constructions were essentially optimal and that the answer was n1+o(1). The model produced an infinite family of configurations exceeding that bound by a polynomial factor.

What happened next is the part that matters here. On the same day, Noga Alon, Thomas Bloom, W. T. Gowers, Daniel Litt and Will Sawin posted a paper whose abstract begins: “We present a short, digested, human-verified version of the recent OpenAI-generated counterexample to the Erdős unit distance conjecture, and a sequence of reflections on it” (Alon et al. 2026). They situated the argument in existing mathematics, attributing its crucial ideas to Ellenberg-Venkatesh, Golod-Shafarevich, and Hajir-Maire-Ramakrishna. Sawin subsequently supplied an explicit constant. Gowers indicated he would recommend the result for the Annals of Mathematics. The claim entered the literature by the ordinary route, and the operative verb in the abstract is digested: five mathematicians converted a machine’s output into a form humans could evaluate, and then evaluated it.

On 1 August 2026 the same laboratory published Ten Advances in Mathematics and Theoretical Computer Science, reporting results from an internal model on ten problems, most open for decades (OpenAI 2026b). The presentation was in one respect far stronger than in May. Every result shipped with a Lean 4 formalization, released under Apache 2.0 as the repository openai/ten-proofs. The project metadata records no unproved steps anywhere in the development and permits only the three standard axioms of the mathematical library, propext, Classical.choice and Quot.sound (OpenAI 2026c). The repository ships configurations for Comparator, an independent checker, with a second independent kernel enabled. By the standard the formal methods community has advocated for forty years, this is close to exemplary.

Four weeks later, the fourth of those results, a claimed counterexample to Connes’s rigidity conjecture, sits in an unresolved dispute. A critique appeared within a day claiming to have traced the entire development and to have found that the constructed groups do not satisfy the infinite conjugacy class condition the conjecture requires. The critique was itself contested: a mathematician at the laboratory rebutted it publicly, commentators identified an apparent error in its group theory, and the document’s provenance came under question, its stated institution appearing to exist only as a website and the text itself appearing machine generated. A separate audit of the critique’s revision history has since been posted. At least three mutually independent machine generated counterexamples to the same conjecture are now in circulation from different laboratories. Some participants in the public discussion resolved the question, to their own satisfaction, by asking language models which side was right.

We take no position on the mathematics. Whether the August construction is correct is not ours to judge and, we will argue, not necessary to judge. The object of interest is the difference in fate. Two claims, one laboratory, one year, comparable stakes; in one case a rapid and conclusive community verdict, in the other a dispute that machine checkable certificates did not settle and may have helped to prolong.

The natural reading is that the May result was easier, or luckier, or that the August results are simply harder to check because there is more of them. We will show that this reading is wrong in an instructive way. Measured directly, the August artefacts present a smaller human reading task per result than the May argument did. The difficulty is not volume. It is that the reading which remains can be done only by a very small number of people, and in August those people were neither recruited nor, as the laboratory’s own metadata records, replaced by anything other than another model.

Our thesis is that this is the general case. Making derivational checking free does not reduce the verification burden attached to a body of knowledge. It transfers that burden onto layers that cannot be mechanized and whose throughput is bounded by the supply of qualified readers, while removing the only limit that previously constrained the rate at which claims arrived. The result is not faster knowledge but a widening gap between what has been certified and what has been adjudicated.

Section 2 sets out the three layer distinction the argument needs. Section 3 recovers the reason, from a debate that ran in the Communications of the ACM between 1979 and 1988, why the middle layer resists mechanization in principle.

Related work. 3 What the 1979 to 1988 debate already settled The problem now being rediscovered was posed and largely resolved, at the level of principle, in an argument that ran through the Communications of the ACM across a decade.

De Millo, Lipton and Perlis (1979) argued that the certainty of mathematics is produced by a social process. A theorem becomes reliable because it is read, doubted, simplified, taught, generalized and used, by many people over time. Formal program verification, they argued, cannot inherit that reliability, because the verifications are long, mechanical and unreadable, and so are never subjected to the process that confers belief. The argument was widely read as hostile to formal methods and has often been treated as refuted by the subsequent success of proof assistants. That reading misses what survives. Their central claim was not that mechanical checking fails; it was that mechanical checking is not the thing that makes mathematics trustworthy, because trustworthiness is a property conferred by readers, and unreadable objects have none.

Fetzer (1988) sharpened the point into a distinction that our L1 and L2 track directly. Formal verification establishes relations among formal objects. It cannot establish the correspondence between a formal object and the extra formal thing it is meant to represent, because that correspondence is not itself a formal relation and so is not the kind of thing a derivation can bear on. In Fetzer’s case the extra formal thing was the behaviour of a physical machine. In ours it is the content of a mathematical question as the discipline understands it, which is transmitted through papers, seminars, examples and usage rather than through any canonical formal text.

This yields what we will call the grounding regress. Suppose we wish to check mechanically that a formal statement S faithfully renders an informal question Q. A mechanical check requires both relata to be formal. So it requires a formal rendering of Q, call it S′. But then the question of whether S′ faithfully renders Q is exactly the question we began with. Either the regress continues or it terminates in an unaided human judgement that some formal object means some informal thing. It always terminates in the latter, because that is the only place it can terminate.

The consequence is stronger than the familiar observation that L2 is hard, or neglected, or not yet automated. L2 is not a task awaiting a better tool. It is the point at which formal method necessarily touches something outside itself, and machine checking’s guarantee, however strong, stops exactly there. Every improvement in automation makes the terminal human judgement more consequential, because more weight rests on it and less independent evidence surrounds it.

Method. 2 Three layers of verification It is useful to separate three questions that the phrase “the proof has been verified” runs together.

L1, derivational validity. Does the proof term type check against the kernel? Every inference is checked mechanically against a small trusted core. This is what a proof assistant does, and it does it very well. The cost of performing an L1 check, given the artefact, tends towards zero and is falling. The August corpus is exemplary at this layer, and we will insist on the point: zero unproved steps, three standard axioms, independently rechecked by a second kernel.

L2, representational fidelity. Does the formal statement, together with every definition it rests on, mean the informal question? This asks whether the sentence the kernel certified is the sentence the field cares about. No compiler checks it. It is checked, if at all, by a human who knows both the mathematics and the formal language, reading the statement and judging.

L3, epistemic significance. Is the result novel, does it matter, is it framed correctly, does it advance the subfield? This is the traditional business of referees and of the discipline over time, and it is not our main subject, though it shares L2’s dependence on scarce human attention.

The three layers differ in three respects that the rest of the paper turns on: in what checks them, a machine, an expert, a community; in whether they can in principle be mechanized, yes, no, no; and in how their cost behaves as the volume of claims rises, falling to zero, roughly constant per artefact, and rising.

Two clarifications forestall predictable objections. First, this is not a claim that proof assistants are untrustworthy. The opposite: the L1 guarantee is the strongest guarantee in the epistemology of mathematics, and the argument here depends on it being strong. Second, the distinction is not new as an observation. Practitioners have always known it, it is discussed carefully in the formalization literature (Avigad 2023; Commelin and Topaz 2023; Bayer et al. 2022), and since August 2026 it has become common currency in public commentary. What is new here is the treatment of the three layers as an economic structure with different scaling behaviour, and the consequences that follow.

The autoformalization programme is the natural place to look for a mechanical solution to L2, and it is worth saying at the outset why it does not supply one. That programme aims to translate informal mathematics into formal statements automatically (Szegedy 2020; Wu et al. 2022), and is evaluated against benchmark suites of paired informal and formal statements (Zheng et al. 2021; Azerbayev et al. 2023). The evaluation is where the difficulty sits. A benchmark of paired statements encodes, in its pairings, precisely the correspondence whose reliability is in question, and those pairings were fixed by human judgement when the benchmark was built. Autoformalization can therefore produce candidate statements at scale, and can be scored against a fixed stock of human judgements, but it cannot certify a correspondence for a question nobody has yet paired. The regress set out in Section 3 applies to it directly.

4 A taxonomy of representational mismatch If L2 must be checked by hand, it is worth knowing what to look for. The following taxonomy is derived from documented incidents in the formalization record and from structural features of the August corpus. We present it as an audit protocol rather than as a catalogue of defects: each category names an obligation an auditor must discharge, not an accusation against any particular development.

T1, quantifier scope displacement. The formal statement binds a variable at a different scope than the informal claim requires. The clearest documented instance comes from the Flyspeck project, the formal proof of the Kepler conjecture and the most carefully executed formalization effort of its generation. Scharf (2017) observed that Hales establishes that the density of a packing within a ball of radius r is bounded by π/ √ T2, reformulation of the target.

Discussion. We can now state the argument compactly.

Let g denote the cost of generating one certified claim, a the cost of a competent L2 audit of one claim, and H the expert reading hours available per period to a given subfield. Certified claims can be produced at a rate bounded by budget divided by g. They can be audited at a rate bounded by H/a.

Machine generation drives g towards zero, and the August corpus reports a per problem inference cost below two thousand dollars at internal rates. Nothing drives a towards zero. The measurements above show why: engineering can compress the artefact, as the challenge file separation did by a factor of 379, but the residue is irreducibly expert, and expertise is what a is made of. Nor does H grow. The population able to audit a claim in von Neumann algebras is fixed on any timescale relevant here, is not compensated for the work, and is drawn from the same people who would otherwise be proving theorems.

Two consequences follow.

The first is the transfer of burden. Total verification work per claim does not fall when L1 becomes free; its composition changes. Before, a reader who checked a proof line by line thereby also checked, in passing, that the statement said something sensible, because reading the argument required understanding the objects. Mechanical checking removes the line by line reading and with it the incidental L2 check that came free with it. The L2 obligation is not reduced by automation; it is isolated by automation, and left standing alone.

The second is the decoupling of certification from belief. As the ratio of produced claims to audited claims diverges, the fact that a claim is certified stops carrying information about whether anyone has judged it to mean what it says. Certification remains a perfectly reliable signal about L1 and becomes an increasingly uninformative signal about the thing a reader actually wants to know.

The observable consequence is what we call adjudication scarcity. When a dispute arises about a certified claim, resolving it requires exactly the resource that has become the bottleneck. If that resource does not appear, the dispute does not resolve; it degrades. The August episode shows the degradation in an unusually complete form. Within four weeks the community had produced a critique of the claim, a rebuttal of the critique, an investigation into the provenance and revision history of the critique’s author, an argument about the existence of that author’s institution, two further machine generated counterexamples to the same conjecture from other laboratories, and at least some participants adjudicating by asking language models. What it had not produced, so far as the public record shows, is one qualified specialist reading the 223 line statement and saying what it means.

This is the sense in which verification abundance produces adjudication scarcity. The claims arrive certified, which makes them hard to dismiss; there are many of them, which makes them hard to prioritize; the qualified readers are unchanged in number and now face a task from which the incidental rewards of reading a proof, learning the technique, have been stripped out. The community’s fallback, when adjudication fails, is testimony, and the available testimony increasingly comes from systems of the same kind that generated the claim.

We note explicitly that this argument does not depend on the outcome of the Connes dispute. If the August construction is correct, the community took more than four weeks and did not establish that it was correct. If it is flawed, the community took more than four weeks and did not establish that it was flawed. Either way the adjudication failed, and it is the failure, not the mathematics, that we are describing.

Conclusion. The formal methods programme has spent forty years arguing that mechanical checking should replace human trust in long arguments, and it has largely won. The August 2026 release is what winning looks like: ten results, no unproved steps, three axioms, an independent kernel, statements separated for audit, metadata published. The L1 problem is solved.

The consequence is not the one the programme anticipated. Solving L1 did not reduce the amount of human judgement mathematics requires. It isolated that judgement, stripped away the incidental checking that used to come free with reading a proof, and removed the constraint that previously limited how fast claims could arrive.