Source-linked AI summary
Verification abundance, adjudication scarcity: what happens to mathematical knowledge when proof checking becomes free
Maher Kallel, Mohamed El Louadi
TL;DR
Machine-checkable proofs can establish derivational validity without settling whether a formal statement means the intended mathematical question or whether a result matters. The paper distinguishes these verification layers, explains why representational fidelity requires human judgment, and argues that making proof checking effectively free shifts work to scarce expert adjudication.
Problem
When derivational checking becomes cheap, it remains unclear how to verify that formal statements faithfully express the mathematical questions they claim to answer.
Source: §2 · p. 3Method
Results
0.263 per cent of the August artefact by size remained an irreducibly expert reading task, which nobody performed in the case examined.
Source: §11 · p. 10Takeaways & Limitations
Machine checking can make derivational verification abundant while leaving adjudication dependent on scarce human attention.
Source: §1 · p. 2, §11 · p. 10The empirical base is two closely matched, unusually well-documented cases from one laboratory in one year, not a representative sample.
Source: §10 · p. 10
Abstract
from arXiv · showhide
In May 2026 an OpenAI model produced a counterexample to the Erd\H{o}s unit distance conjecture. Five mathematicians published a human-verified version the same day, and the result entered the literature within weeks. In August 2026 the same laboratory published ten mathematical and theoretical computer science results, each accompanied by a machine-checkable Lean 4 certificate with no unproved steps. Four weeks later, one remained the subject of an unresolved dispute over whether its formalization meant what it claimed. We argue that this difference is structural. We distinguish three layers of verification: derivational validity, which a kernel checks; representational fidelity, whether the formal statement means the intended question; and epistemic significance. Only the first is mechanizable. Making it effectively free therefore does not eliminate verification work but shifts the burden to layers dependent on scarce expert attention. Measurements of the August corpus illustrate the shift. The kernel-checked proofs total 20.6 MB, while the statements requiring human audit total 55.6 KB, a ratio of 379 to 1. Yet those statements contain 218 bespoke definitions rather than relying on community-vetted ones. The audit surface is therefore small in volume but irreducibly expert. We argue that machine checking produces verification abundance while leaving adjudication scarce. We propose a six-category taxonomy of representational mismatch, a disclosure schema for machine-generated mathematical claims, and implications for software, cryptography, and regulated decision systems.
1 Two results, two fates
The May counterexample was digested and evaluated by mathematicians, while the August results arrived with strong machine-checkable certificates but one remained disputed. The paper argues that the difference reflects scarce expert adjudication, not a larger reading task.
1 Two results, two fates
- Five mathematicians published a human-verified version of the May counterexample the same day, and the claim entered the literature by the ordinary route.They situated the argument in existing mathematics, and Sawin later supplied an explicit constant.Source: §1 · p. 2
- The August release supplied Lean 4 formalizations for ten results with no unproved steps, three standard axioms, and an independent kernel check.The authors call this close to exemplary by the formal methods community’s standard.Source: §1 · p. 2
- Four weeks later, the claimed Connes rigidity counterexample remained in a contested dispute over whether the constructed groups met the conjecture’s infinite conjugacy class condition.The critique and its rebuttal were themselves contested, and multiple machine-generated counterexamples were in circulation.Source: §1 · p. 2
- The paper argues that the August artefacts require a smaller human reading task per result than the May argument, but that task can be done only by a very small number of people.The August metadata recorded another model, not recruited human readers, as the replacement for that expert attention.Source: §1 · pp. 2–3
- The authors frame the contrast as a widening gap between certified claims and adjudicated knowledge when derivational checking becomes free.They describe the cases as closely matched in stakes and from one laboratory in one year.Source: §1 · pp. 2–3
2 Three layers of verification
The paper separates verification into derivational validity, representational fidelity, and epistemic significance. Only the first is mechanically checked; the other layers depend on human expertise or community judgment.
2 Three layers of verification
- L1 asks whether a proof term type-checks against a kernel, which checks every inference and can be independently rechecked at near-zero cost.The August corpus had zero unproved steps and three standard axioms.Source: §2 · p. 3
- L2 asks whether the formal statement and its definitions mean the informal question the field cares about, a judgment requiring a human who knows both mathematics and the formal language.No compiler checks this correspondence.Source: §2 · p. 3
- L3 asks whether a result is novel, important, properly framed, and advances its subfield; referees and the discipline over time judge it.Like L2, it depends on scarce human attention.Source: §2 · p. 3
- As claim volume rises, the three layers are checked by machines, experts, and communities, with costs respectively falling to zero, roughly constant per artefact, and rising.The authors treat these distinct scaling behaviors as an economic structure, not a new observation that the layers differ.Source: §2 · p. 3
- Autoformalization can generate candidate statements at scale and score them against fixed human-judged benchmarks, but cannot certify correspondence for a question not already paired.The benchmark pairings themselves encode human judgments of the correspondence under evaluation.Source: §2 · p. 4
3 What the 1979 to 1988 debate already settled
The paper revisits arguments that mathematical trust comes from social reading and that formal checking cannot establish correspondence to what a formal object represents. It applies this reasoning to machine-generated mathematical claims, whose production need not be bounded by human capacity.
3 What the 1979 to 1988 debate already settled
- De Millo, Lipton and Perlis (1979) argued that mathematical reliability is produced through social reading, doubt, simplification, teaching, generalization, and use over time.They held that mechanical, unreadable verifications do not undergo this process, while conceding that mechanical checking itself need not fail.Source: §3 · p. 4
- Fetzer (1988) argued that formal verification relates formal objects but cannot establish their correspondence to an extra-formal object; here, that object is a mathematical question understood through disciplinary practice.The paper transposes Fetzer’s account from physical-machine behaviour to disciplinary mathematical meaning.Source: §3 · pp. 4–5
- The grounding regress arises because mechanically checking that a formal statement S faithfully renders an informal question Q requires a formal rendering S′, whose own fidelity to Q raises the original question again.The regress terminates only in unaided human judgment that a formal object means an informal thing.Source: §3 · p. 4
- The authors argue that L2 is a necessary point where formal method meets something outside itself, so stronger automation makes the terminal human judgment more consequential.They say less independent evidence surrounds that judgment as more weight rests on it.Source: §3 · p. 4
- The paper’s contribution is to make the older argument quantitative for machine-generated mathematics, where certified claims need not be bounded by the number of people willing to produce them.It distinguishes this transposition from the earlier argument it attributes to Fetzer.Source: §3 · pp. 4–5
4 A taxonomy of representational mismatch
The paper presents six types of representational mismatch as an audit protocol: obligations for checking whether formal statements capture intended informal questions, not accusations of defects. The taxonomy is not claimed to be exhaustive.
4 A taxonomy of representational mismatch
- The taxonomy draws on documented incidents and August-corpus features but is not exhaustive; the authors claim it is sufficient to structure an audit.They distinguish it from Mao et al. (2026), which addresses whether a formal proof mirrors natural-language reasoning rather than statement-level mismatch.Source: §4 · pp. 5–6
- T1, quantifier scope displacement, occurs when a formal statement binds a variable at a different scope than the informal claim requires.In the Flyspeck example, the formal bound uses a constant depending on the packing, whereas the intended statement requires one independent of the packing; the kernel does not reveal the difference.Source: §4 · p. 5
- T2, reformulation of the target, uses a tractable surrogate whose equivalence to the informal statement must be recovered through an informal audit.Flyspeck formalized density in finite containers with an error term vanishing relative to container volume, then recovered the traditional statement in the limit.Source: §4 · p. 5
- T3, bespoke definitional substitution, replaces a community-vetted standard notion with a local definition, adding a dictionary the auditor must read.The August corpus introduced 218 local definitions across twelve statement files.Source: §4 · p. 5
- T4, domain or universe restriction, narrows the quantified class, as when the Connes statement restricts Hilbert-space representations to the group’s universe.For a group in the lowest universe, this limits the representations considered; whether it is harmless requires expert judgment.Source: §4 · p. 5
- T5, hypothesis satisfied by construction rather than content, concerns whether lemmas proving a formal predicate apply to the construction actually used.In the Connes dispute, the infinite conjugacy class condition is present and defined standardly; the dispute concerns whether the lemmas apply to the construction.Source: §4 · pp. 5–6
- T6, encoding substitution, arises when computational claims rely on bespoke encodings of machines, languages, or complexity classes.The August closest vector problem statement locally defines bit-level Turing machines, verifiers, and NP membership in forty definitions.Source: §4 · p. 6
5 The audit surface: measurements
The August corpus sharply compressed the material requiring human reading, but its statements introduced many local definitions that made auditing an expert task. The repository also recorded agent review rather than human domain-expert review, unlike the May case.
5 The audit surface: measurements
- 379 to 1: the August proof corpus was 20.6 MB, while statements for human audit totaled 55.6 KB.Those statements were 0.263% of the released Lean, and the contested Connes statement was 7,483 bytes across 223 lines.Source: §5 · p. 6
- 218 local definitions supported 38 theorem statements, requiring auditors to compare bespoke terms against their standard meanings.The Connes statement alone used 22 local definitions, including definitions of the infinite conjugacy class condition and property (T).Source: §5 · pp. 6–7
- The repository marked the development agent-reviewed, and laboratory records said no human domain expert checked representational fidelity.The audit surface was small in volume, but validating its private mathematical vocabulary required specialist expertise and fluency in Lean.Source: §5 · p. 7
- The May argument received a human-verified version from five mathematicians within a day, while the August release put a machine in the reviewer’s chair for twelve declarations.The authors characterize the difference in outcome as following this contrast.Source: §5 · p. 7
6 The inversion
When machine generation drives the cost of certified claims toward zero, expert auditing remains bounded by available reading hours. The resulting gap separates certification from adjudication and leaves disputes unresolved when qualified readers do not appear.
6 The inversion
- As generation cost g approaches zero, certified claims can arrive faster than audits bounded by H/a, where H is available expert reading time and a is audit cost.The August corpus reported an internal inference cost below $2,000 per problem, while the authors argue that expertise and available audit hours do not similarly scale.Source: §6 · p. 7
- Making derivational checking free does not reduce total verification work; it isolates the representational-fidelity obligation that proof reading once checked incidentally.The line-by-line reading disappears, but the obligation to judge whether the statement says something sensible remains.Source: §6 · p. 7
- As produced claims outnumber audited claims, certification remains reliable about derivational validity but becomes less informative about whether anyone judged what a claim means.The paper calls this decoupling of certification from belief.Source: §6 · p. 7
- When disputes require scarce expert judgment, they can degrade without resolution into rebuttals, provenance disputes, and reliance on language models for adjudication.The public record showed no qualified specialist had read the 223-line statement and said what it meant.Source: §6 · p. 8
- The argument does not depend on whether the Connes construction is correct: after more than four weeks, the community had established neither its correctness nor its flaw.The authors describe the failure to adjudicate, not the mathematical outcome.Source: §6 · p. 8
7 What good engineering reaches, and what it does not
The August release used conscientious engineering to strengthen derivational checking and make statements easier to inspect. Those measures did not settle whether the formal statement captured the intended conjecture, and bespoke definitions expanded the audit burden along an expertise dimension.
7 What good engineering reaches, and what it does not
- The release had no unproved steps, used only three standard axioms, separated statements from proofs, supported an independent kernel, and disclosed agent-reviewed status.The statement/proof separation reduced the audit surface by a factor of 379.Source: §7 · p. 8
- Comparator can verify that a proof establishes its challenge statement, but cannot determine whether that statement is Connes’s conjecture.Separating the statement from the proof makes human reading more tractable; it does not perform the terminal judgment.Source: §7 · p. 8
- The 218 local definitions compressed the statements in bytes but expanded the expertise needed to audit them, limiting the practical effect of size reduction.Using existing library definitions would make statement files larger while reducing the audit surface in the sense that matters.Source: §7 · pp. 8–9
8 Transfer
The authors extend the specification-to-intent problem beyond mathematics to software, cryptography, and regulated decision systems. They recommend treating generators as hypothesis producers, keeping checkers independent, and explicitly staffing specification review.
8 Transfer
- In software and cryptography, a machine-checked proof that an implementation meets a specification does not establish that the specification captures the intended security property.The authors argue that specification review becomes a binding constraint as machine-generated code grows and formal pipelines mature.Source: §8 · p. 9
- For regulated decision systems, a mechanical pass must not be reported as though it settled a question of meaning.The authors describe these settings as having a weaker mechanical layer and a stronger institutional one.Source: §8 · p. 9
- The recommended response is to treat generators as hypothesis producers, keep checkers independent, and assign named people and time to specification review.The authors identify specification review as the layer likely to fail silently if it is not explicitly staffed.Source: §8 · p. 9
9 Remedies
The remedies propose disclosure of information needed to estimate audit demand, a named role for statement review, and graded assurance levels for scrutiny.
9 Remedies
- Machine-generated discovery claims should disclose attempts, selection, total inference spend, review hours and qualifications, and which definitions are local rather than library imports.Without attempted-problem counts, outsiders cannot calculate success rates or estimate audit capacity against generation capacity.Source: §9 · p. 9
- The paper proposes naming and crediting statement reviewers, whose domain expertise and formal fluency are distinct from proof refereeing.Journals accepting formalized results should require and record this review; the authors suggest it be paid where institutions can manage it.Source: §9 · p. 10
- Assurance could range from kernel checking alone to a printed argument for the informal-to-formal correspondence, with named expert review as an intermediate level.The August release is characterized as kernel-checked with statements separated for independent audit; the May result reached the fourth level through human digestion.Source: §9 · p. 10
10 Limitations
The evidence is limited by its narrow case base, proxy measurements, and unvalidated taxonomy, while the fixed-capacity assumption applies to a transition rather than a long-run steady state.
10 Limitations
- The empirical base comprises two unusually well-documented, closely matched cases from one laboratory in one year, not a representative sample.Source: §10 · p. 10
- Published-artefact measurements do not capture unpublished internal review, and recorded agent-review metadata does not prove that no human read the statements.Source: §10 · p. 10
- Byte counts are a crude reading-effort proxy, while the reproducible local-definition count does not weight definitions by difficulty.A fuller analysis would count tokens and grade definitions by depth.Source: §10 · p. 10
- The incident-based taxonomy has not been systematically validated on a large corpus, and fixed expert-audit capacity is an assumption about years rather than decades.Formal fluency among mathematicians is rising over decades; the argument concerns the transition, not the steady state.Source: §10 · p. 10
11 Conclusion
The conclusion is that mechanized proof checking has succeeded at derivational validity but has not removed human judgment. By uncoupling claim production from the supply of readers, it leaves adjudication as the scarce resource.
11 Conclusion
- The August release exemplifies the formal-methods programme's success: ten results have no unproved steps, use three axioms, and have an independent kernel.Source: §11 · p. 10
- Solving L1 isolates rather than eliminates human judgment, leaving a small statement-reading task that remains irreducibly expert.That task is 0.263 per cent of the artefact by size and nearly all of it by difficulty; in the examined case, nobody performed it.Source: §11 · p. 10
- The supply of certified claims and the supply of readers once scaled together because both required people, but that coupling is now broken.The conclusion reframes the earlier debate: mechanization works, yet its proof objects can remain unread.Source: §11 · pp. 10–11
- The scarce resource in mathematical knowledge production is adjudication, not proof.Source: §11 · p. 11