Agent swarms do mathematics: CFSG in Lean, ETH refuted, and the counterpoint

TL;DR. Axiom formalized the Classification of Finite Simple Groups (about 15,000 pages across 500+ papers) into roughly 40 million lines of Lean in 24 days, with agent swarms writing and mathematicians steering; 2,000+ mistakes caught along the way. Axiom credits co-designing models, harness and infrastructure. ETH: OpenAI and Anthropic models independently found a 2^(n/√log n) algorithm for 3-SAT, refuting the 27-year-old Exponential Time Hypothesis if it holds; OpenAI has sent its ETH, Kakeya and Yang-Mills results to outside reviewers including a Nobel laureate (The Decoder). The Information notes both labs claimed a cryptography breakthrough the same day. Counterpoint: a DeepMind position paper ("LLMs Can't Jump") argues models lack abduction and proposes grounded world models.

Relation to prior wiki pages

• Agent harness engineering: Axiom's credit to harness and infra co-design is the strongest production example yet of the harness thesis.
• If ETH falls, hundreds of fine-grained complexity results lose their foundation; this is a review-pending claim.

Sources: Axiom · The Decoder · The Information