CFSG fully formalized in Lean: 43.1M lines, and a flaw found in a published proof
ChrSzegedy · x · 2026-11-03
Axiom Math announced a complete Lean formalization of the Classification of Finite Simple Groups, following the first-generation proof with every step checked by Lean's kernel. The project spans 43.1M lines of Lean, 2.05M declarations, 715 cited works, and 100 milestones. Along the way, the team found counterexamples to a closure assertion in a published argument for the Unbalanced Group Theorem; an accompanying paper explains the obstruction and gives an alternative route built on Solomon's 1976 theory of maximal 2-components. The classification itself stands.
More from Research
- Counting mRNAs in living bacteria: the 2005 Golding paper that overturned the Poisson model of transcription — NikoMcCarty · 2026-11-03
- AAAI 2027 to host Neuro for AI & AI for Neuro workshop in Montreal, papers due in 3 weeks — naturecomputes · 2026-11-03
- DeepSeek V4.1 Flash 1017 doubles ARC-AGI-3 score to 5.81%, leads open models — teortaxesTex · 2026-11-03
- Critics tear apart "Weight-Space Programming": Atari test spoon-feeds answers, Qwen case fails on Gemma — anshulkundaje · 2026-11-03
- Cohere paper: adjacent tokens share 20-45% of experts, making speculative decoding cheap even at batch size 1 — rohanpaul_ai · 2026-11-03
- Editing 131k weights to fix looping: activation steering yields free benchmark gains — xennygrimmato_ · 2026-11-03