Is a finite free group scheme killed by its order?

A finite free group scheme of order four not killed by four

Model / AI: Codex, Claude

a counterexample to Grothendieck's 60-year-old question, constructed and formalized with Codex and Claude and merged into mathlib; Buzzard's account credits Mathew and Alpöge and reports he compiled the file himself.

Source review pending. Imported from the original notes; linked claims and artifacts have not been re-audited in this restructuring.

• Lean — A finite free group scheme of order four not killed by four
• Context — account