AI-assisted counterexample answers Grothendieck's question on finite flat group schemes, merged into Mathlib
Akhil Mathew, using OpenAI's and Anthropic's models, found a finite locally free group scheme of order 4 over a non-reduced finite ring with 2⁹ elements that is not killed by 4 (it is killed by 8). This answers Grothendieck's question negatively. The Lean proof was merged into Mathlib on 3 Aug 2026.
Key facts
- Known positive cases: commutative (Deligne), reduced base (Grothendieck); pure characteristic-p case still open
- Found by studying deformations of α₂×α₂
- Kevin Buzzard attributes discovery to OpenAI's Sol and autoformalisation to Claude Fable
- Mathlib PR #41748 (Counterexamples/GrothendieckPower.lean), merged 3 Aug 2026
Science result
- Field
- mathematics / algebraic geometry / group schemes
- Problem
- Grothendieck's question: is every finite locally free group scheme of order n killed by n?
- Result
- A counterexample of order 4 not killed by 4, over a non-reduced base.
- AI system
- GPT-5.6 Sol, Claude Fable 5
- Human role
- AI-assisted: Akhil Mathew directed the search and verified
- Verification
- Formal proof in Lean (Mathlib)
- Status
- confirmed
What happened
In the same weeks as the Jacobian counterexample, Mathew used frontier models to find and formalise a counterexample to a question from the foundations of algebraic geometry.
Why it matters
Kevin Buzzard said this mattered more to him than the Erdős results because it lies in "an area of mathematics that I personally find more interesting". AI was now reaching core modern algebraic geometry.
Changelog
- 2026-09-29: created
Related events
Sources (2)
- discussionBenjamin Antieau: Akhil Mathew and AI
- discussionXena Project: Human mathematicians are being out-counterexampled
id: 2026-07-01-grothendieck-group-scheme-counterexample · updated 2026-09-29 · open in the interactive timeline