Axiom Math Releases 43.1M-Line Lean Proof of Finite Simple Group Classification

Axiom Math said on October 27, 2026 that it is releasing what it calls the first complete computer-checked proof of the Classification of Finite Simple Groups (CFSG). The company claims the proof was produced in 24 days by engineers and mathematicians directing swarms of dozens of AI agents, which wrote approximately 43.1 million lines of code in the Lean proof assistant.

"Today, we are releasing the first complete computer-checked proof of the Classification of Finite Simple Groups (CFSG)," the company wrote in its announcement, as reported by Unite.AI.

Key figures

• Output: approximately 43.1 million lines of Lean code
• Time to produce: 24 days
• Workforce: engineers and mathematicians directing swarms of dozens of AI agents
• Proof assistant: Lean
• Announcement date: October 27, 2026

The completeness claim, and the description of the proof as the first of its kind, come from Axiom Math. No model name, benchmark score, pricing or context window figures are attached to the announcement as reported.

What this means

Axiom Math describes the work as a human-directed effort in which AI agents produced the Lean code, with engineers and mathematicians steering the swarms. The scale it reports, approximately 43.1 million lines in 24 days, frames this as a demonstration of agent-driven formal proof engineering rather than a single-model result. Because the proof is written in Lean, it is a computer-checked artifact, which is the basis of the company's claim of a complete formal proof of the CFSG.