Elliot Glazer(@ElliotGlazer):1. Congrats for formalizing CFSG! Imo the importance here is that this is a blackbox result for which a mere "truth certificate" is intrinsically valuable and adds confidence to many results atop. 2. The biggest correction was of a wrong proof of UGT, which already had other proofs since then. I think this largely justifies the common wisdom "There are mistakes in the literature, but CFSG has long been proven."

2026.10.27 18:57

1. Congrats for formalizing CFSG! Imo the importance here is that this is a blackbox result for which a mere "truth certificate" is intrinsically valuable and adds confidence to many results atop. 2. The biggest correction was of a wrong proof of UGT, which already had other proofs since then. I think this largely justifies the common wisdom "There are mistakes in the literature, but CFSG has long been proven."

Axiom@axiommathai

2026.10.27 14:34

The largest math proof in human history is now computer-verified. Today, Axiom announces a complete Lean auto-formalization of the Classification of Finite Simple Groups, the "periodic table of symmetry." About 15,000 pages, built by over 100 mathematicians across generations.