SOURCE-LINKED INTELLIGENCE

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

arXiv · AI, language, vision and robotics · article · Aug 29, 2026 · UTC

In May 2026 an OpenAI model produced a counterexample to the Erdő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 v

Read original source ↗ Open in workspace

recordType

paper

region

Global