Human mathematicians are being outcounterexampled
20 hours ago
- ChatGPT disproved Erdős’ Unit Distance conjecture; human mathematicians validated it, but initially, it wasn't formalized in Lean.
- Logical Intelligence autoformalized the counterexample in Lean, and Boris Alexeev achieved a full Lean formalization using OpenAI's Sol model, generating 1.2 million lines of Lean code in three weeks.
- During a workshop, an AI-generated exposition on finite flat group schemes contained a false claim; AI identified and provided a counterexample to it.
- AI, via Sol and Fable, found a counterexample to Grothendieck's question on group schemes of order n. Akhil Mathew formalized it in Lean, and it was added to mathlib.
- AI tools like Sol and Fable enabled rapid progress in formalizing mathematical projects, such as modularity lifting theorems, and are becoming essential for researchers.
- Fable found a counterexample to the Jacobian Conjecture, a long-standing open problem. Paul Lezeau formalized it, and DeepMind's repository facilitated verification.
- AI-generated mathematics requires formal verification for trust, but understanding the insights from counterexamples remains a key challenge for human mathematicians.