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

arXiv: https://arxiv.org/abs/2608.28997 · HTML: https://mlsanity.com/paper/2608.28997/

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 6 of its 17 references that are in the map.
- First posted on arXiv 29 Aug 2026.

## Builds on (most cited first, 6 of 6)

- [MiniF2F: a cross-system benchmark for formal Olympiad-level mathematics](https://mlsanity.com/paper/2109.00110/) (2021)
- [Autoformalization with Large Language Models](https://mlsanity.com/paper/2205.12615/) (2022)
- [ProofNet: Autoformalizing and Formally Proving Undergraduate-Level Mathematics](https://mlsanity.com/paper/2302.12433/) (2023)
- [Abstraction boundaries and spec driven development in pure mathematics](https://mlsanity.com/paper/2309.14870/) (2023)
- [Mathematical Proof Between Generations](https://mlsanity.com/paper/2207.04779/) (2022)
- [Does the Proof Prove It That Way? Faithful Formalization of Elements Proofs](https://mlsanity.com/paper/2608.15432/) (2026)

## Abstract (arXiv)

In May 2026 an OpenAI model produced a counterexample to the ErdHos 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.