AI Outpaces Human Mathematicians with Counterexamples
Original: Human mathematicians are being outcounterexampled
Why This Matters
AI systems are now autonomously formalizing major mathematical proofs at a scale and speed that surpasses traditional human workflows.
In May 2026, ChatGPT disproved Erdős' Unit Distance conjecture in discrete geometry. By June 26, OpenAI's model Sol produced a complete 1.2-million-line Lean formalization of the proof in three weeks, covering hard theorems in global class field theory.
On May 20, 2026, ChatGPT disproved the long-standing Erdős Unit Distance conjecture by leveraging the Golod-Shafarevich theorem from 1960s number theory. Human mathematicians with early access vouched for the argument. Within a week, Logical Intelligence — co-founded by Turing Award winner Yann LeCun and with Fields Medallist Mike Freedman as CSO — autoformalized the ChatGPT-generated paper in Lean, specifically verifying that the number-theoretic theorem implied the counterexample. However, the underlying Golod-Shafarevich theorem itself (100+ pages, requiring global class field theory) remained unformalized. That changed on June 26, 2026, when Boris Alexeev of OpenAI announced that OpenAI's new model Sol had produced a complete Lean formalization of the Erdős counterexample from first axioms. Sol generated 1.2 million lines of Lean code over three weeks — more than half the size of the entire mathlib library, which took nine years to build. Kevin Buzzard, a mathlib maintainer and author of the Xena Project blog, noted that Sol's output included proofs of difficult global class field theory theorems. Buzzard stated he ran the code in a sandbox due to security concerns about AI-generated code executing arbitrary commands.