Counterexample to Grothendieck's question on finite flat group schemes
Counterexample to Grothendieck's question on finite flat group schemes is graded formally verified on whataifound.org, with the AI's role graded collaborative.
A finite locally free group scheme of order four whose fourth power map is not trivial, answering a question Grothendieck raised in the 1960s; one model produced the construction and another formalised it in Lean.
- Verification
- Formally verified
- Autonomy
- Collaborative
- Lab
- Independent
- Model
- OpenAI Sol (construction); Claude Fable (Lean formalisation)
- Field
- Mathematics
- Date
- 2026-07-11
- Human collaborators
- Akhil Mathew, Kevin Buzzard
What was found
Grothendieck asked whether every finite locally free group scheme of order n is killed by n. Deligne proved it for commutative group schemes; the non-commutative case stayed open. The counterexample is a Hopf algebra of rank four over the ring Z[a,b]/(a³, b³, a²b+2), with coordinate algebra R[U,V]/(U² − abU + b²V, V² − a²V), whose fourth convolution power is not the convolution unit. Kevin Buzzard, told of a 12-page informal write-up, replied that he does not read AI-generated informal mathematics and asked for a Lean proof instead; four hours later a 1,076-line Lean formalisation existed, and it compiles on a laptop in under five minutes. It was submitted to mathlib as pull request #41748.
Novelty check
Per Buzzard's account, the question had been settled in special cases by Grothendieck, Deligne and René Schoof, with further partial results published by Emiliano Torti in 2025; no counterexample appeared in the literature. The object here is an explicit new construction rather than a rediscovered example, and the Lean file states and refutes the general claim directly.
Caveats
The mathlib pull request was open, not merged, when this entry was written, and was filed by a pseudonymous account whose module docstring credits "Codex (OpenAI) and Claude (Anthropic), under the direction of the author" rather than naming Sol or Fable; the model attribution here follows Buzzard's blog post. The `formal` grade rests on the Lean proof compiling, which Buzzard reports doing himself; the 12-page informal argument has not been peer reviewed. Autonomy graded collaborative: a human posed the question, directed the work and filed the PR, and the record of who did which step is a blog post rather than a transcript.
Independent checks
Kevin Buzzard (compiled the Lean formalisation): confirmed; 1,076-line Lean proof compiles in under five minutes · link ↗
Sources
How this is graded
whataifound.org grades every entry on two axes: verification (how solid the result is, from a machine-checked proof down to refuted) and autonomy (how much the AI did versus its human collaborators). This finding is formally verified and collaborative. Full definitions are in the methodology.
Cite this entry
whataifound.org (2026). Counterexample to Grothendieck's question on finite flat group schemes. whataifound.org: A Registry of AI Scientific and Mathematical Discoveries. https://whataifound.org/finding/2026-07-11-grothendieck-group-schemes