Bitter Lessoned in Automated Theorem Proving

gist

John Loeber recounts building a Lean-only automated theorem prover in 2026, then watching base-model gains make it obsolete. He wrote a private Lean4 fork, a multi-agent harness and C++ counterexample search, generating a few hundred thousand lines of Lean toward the degree-57 Moore graph problem and the Hadwiger Conjecture. GPT-5.6 Sol and GPT-6 Astra each helped, then OpenAI's math repo, from an unreleased model run on 4,000 problems at about 3.5 hours of compute each, disproved Hadwiger. He concludes that mathematics now splits into humanities-like study and AI-driven discovery.

ideas

• Base-model gains erased the engineering. Loeber calls the bitter lesson visceral even for someone long convinced of it, and says he has not open-sourced his harness or Lean theorems because models will soon do better for pennies.
• Each model step was visible on hard math. GPT-5.5 proved some novel theorems slowly, Sol produced more correct statements, and Astra brought better proof intuition; he notes these are impressions, not measured evals.
• OpenAI's run was cheap per problem. The math repo came from about 3.5 hours of ChatGPT-Pro-Thinking-equivalent compute per problem, which he estimates at $100 at most, and its Hadwiger disproof is probabilistic rather than a specific counterexample.
• Formalizing after the fact surprised him most. He had built entirely in Lean to keep models on course, but the lab proofs appear to have been written in plaintext with about half formalized later, an observation he marks as unconfirmed.
• The human-AI collaboration window lasted one summer. He credits Levent Alpöge's Jacobian counterexample as its high point and expects the same shift to reach other disciplines.

quotes