AI
Axiom says AI agents computer-checked the largest proof in mathematics
Axiom Math says it has released the first complete computer-checked proof of the classification of finite simple groups, a result written by roughly 100 mathematicians across some 15,000 pages and more than 500 articles. Engineers directed swarms of AI agents that produced about 43.1 million lines of code in the Lean proof assistant over 24 days. Axiom describes the release as a formalisation of the first-generation proof in which every step is checked by Lean's kernel, and says the work surfaced substantive corrections to the literature.