[Перевод] Агенты Axiom Math доказали полноту классификации конечных простых групп всего лишь в 41,3 млн. строчках кода Lean
On October 26, 2026, Axiom Math announced it had completed a full formalization of the Classification of Finite Simple Groups theorem. The theorem is known internationally as CFSG. It lists all the building blocks that make up finite simple mathematical groups. The headline says Axiom Math’s agents proved completeness in just 41.3 million lines of Lean code.
26 октября 2026 года компания Axiom Math сообщила о завершении полной формализации Теоремы о классификации простых конечных групп . В международном математическом сообществе теорема известна как CFSG — Classification of Finite Simple Groups. Эта фундаментальная теорема перечисляет все строительные блоки, из которых состоят конечные простые математические группы. Теорема утверждает, что любая конечная простая группа относится только к одному из четырех типов и никаких других типов конечных простых групп не существует. В текущем виде доказательство занимает более 15 тысяч страниц, разбросанных по более чем 500 статьям. За это теорему о классификацию прозвали Огромной теоремой. Читать далее