Axiom afirma que agentes de IA formalizaram a Classificação dos Grupos Simples Finitos em Lean

Axiom, uma empresa de matemática com IA, anunciou no X uma formalização automática completa em Lean da Classificação dos Grupos Simples Finitos, um resultado que chama de “tabela periódica da simetria”. A empresa descreve a prova original como tendo cerca de 15 mil páginas, escrita por mais de 100 matemáticos ao longo de gerações, e a chama de maior prova matemática da história verificada por computador.

Segundo o repositório de código aberto da Axiom, enxames de agentes de IA produziram cerca de 43,1 milhões de linhas de Lean em 24 dias, abrangendo 715 artigos e livros, e sinalizaram 34 divergências em relação ao registro publicado. Uma publicação da conta de notícias sobre IA TestingCatalog acrescenta que os agentes dividiram o trabalho como equipes de software e escreveram código mais rápido do que o Lean conseguia verificar.

Esses números são um relato da própria Axiom; o anúncio não inclui uma revisão independente da formalização. Até 28 de outubro, a publicação tinha cerca de 6.200 curtidas no X.