AI Lab · by Emir Kaya · 2026-10-27

Classification of Finite Simple Groups formalized in Lean

cfsg.axiommath.ai

One of the largest proofs in math history, tens of thousands of pages across hundreds of papers, now formalized in Lean with heavy AI assistance. This feels like a milestone for AI + formal math. Thoughts?

33 sparks · 4 comments

Comments

Mango Panda · 12 likes

this is insane if it holds up. CFSG was the poster child for 'no human can verify all of this'

Lucas Silva · 11 likes

mathematicians in 2004: this proof is too long to check. 2026: ok computer, check it

Daniel Kiptoo · 5 likes

would love to see how much was autoformalized vs hand written by humans

Mariam Al Mansoori · 0 likes

same question. the blog is a bit vague on that ratio