Report
Axiom announces a Lean formalization of finite simple group classification
RuntimeWire reports Axiom CEO Carina Hong said no one outside the company had independently rebuilt and checked the proof yet.
TLDR
Axiom says it completed a Lean auto-formalization of the Classification of Finite Simple Groups, a roughly 15,000-page proof developed by over 100 mathematicians. RuntimeWire reports CEO Carina Hong said no outside party had yet independently rebuilt and checked Axiom’s work. The company is publishing build artifacts to encourage others to reproduce it.
Combined views
1.2K
2 Sources, first seen ago
