Human mathematicians are being outcounterexampled
Human mathematicians are being outcounterexampled
By Xena — Exploring the frontier of Lean and AI-driven mathematics.
The Current State of Formalization
The last few weeks have provided a fascinating glimpse into the evolving relationship between human mathematicians, AI tools, and the art of the counterexample. This post outlines my observations on how the landscape of formalization is shifting.
The Unit Distance Breakthrough
On May 20, 2026, a significant milestone was reached: ChatGPT successfully disproved Erdős’ Unit Distance conjecture in the field of discrete geometry.
The validity of this claim was supported by several human mathematicians—some of whom are personal acquaintances and trusted experts—who reviewed the argument via early access and verified its logic. The core of the proof relies on a sophisticated result from the 1960s:
For nearly a decade, I have operated under a specific philosophy: I stopped trusting the technical minutiae provided by human mathematicians and turned toward Lean and Interactive Theorem Provers (ITPs) as the essential future of mathematical verification. Naturally, my first instinct was to ask: Has this been formalized in Lean?
The Path to Autoformalization
Shortly after, on May 26, 2026, I heard from Mike Freedman (Fields Medallist and Chief Science Officer at Logical Intelligence, co-founded by Yan LeCun). Mike revealed that their system had already autoformalized the ChatGPT paper. Specifically, they had formalized the logical bridge: that the aforementioned number theory theorem indeed implies the Erdős counterexample.
"Breakthrough LLM-generated mathematics being formalized in real time."
However, a massive hurdle remained—the "elephant in the room." The Golod-Shafarevich theorem is a behemoth, spanning over 100 pages and requiring deep integration of global class field theory.
Historically, this was a daunting task:
- 2025: I co-ran a Clay Summer School with Richard Hill on formalizing class field theory.
- 2026: We have nearly completed the local case (via my student Edison Xie), but the global case was still considered
a fantasynearly impossible to compress or formalize quickly.
The "Sol" Revolution
Everything changed on June 26, 2026. Boris Alexeev (OpenAI) announced on the Lean Zulip that he had used a new model called Sol to achieve a complete formalization of the Erdős counterexample, relying solely on basic mathematical axioms.
The scale of this achievement was staggering. I analyzed the public code and discovered that Sol had managed to prove incredibly difficult theorems regarding the cohomology of number fields.
Production Comparison: AI vs. Human
| Entity | Lines of Lean Code | Timeframe | Notes |
|---|---|---|---|
| mathlib | 2.3 Million | 9 Years | Human-led community effort |
| Sol (AI) | 1.2 Million | 3 Weeks | Generated for a single project |
At this point, the reality became clear: massive, AI-generated mathematical developments are now inevitable.
Because AI code can be unpredictable, I executed it within a secure sandbox to prevent any malicious commands from affecting my system.
-- Warning: Lean is a programming language.
-- Always run untrusted AI-generated Lean code in a sandbox!
#check (theorem_from_sol_model)
The Formalizing Fermat Workshop
In early July, I organized the Formalizing Fermat workshop, sponsored by Logos Research. Like other firms (Harmonic, Axiom AI, Moonshot AI), Logos possesses tools capable of translating natural language mathematics into Lean.
The Tooling Ecosystem
Due to capacity limits on the Logos system (5 users at a time for 25 attendees), I ensured everyone had access to a variety of LLMs:
- Logos Research Tool: Available all week.
- Claude Max (Fable): Provided via subscription.
- ChatGPT Pro (Sol): Provided by OpenAI (released July 9th).
The Irony of the Counterexample
I wanted to develop the theory of finite flat group schemes in Lean to support my ongoing work on Fermat’s Last Theorem. To prepare, I used Fable and ChatGPT to synthesize an exposition of the theory based on classic papers.
I provided this LLM-generated PDF to Logos Research. On the first day of the workshop, Logos informed me that one of the claims in the PDF was false and provided an explicit counterexample.
Upon review, it was evident that the natural language generated by the LLMs had hallucinated or erred during the description of a standard construction.
Summary of Events
The takeaway: While AI can now generate millions of lines of formal code and solve conjectures, it can still stumble in natural language—and it is the formal tools that are now "outcounterexampleing" the AI's own prose.
Workshop Participants & Contributors:
