Agentes de IA da Axiom formalizam a classificação de grupos finitos simples em Lean

A Axiom Math afirmou em 26 de outubro de 2026 que lançou a primeira prova completa verificada por computador da Classificação de Grupos Finitos Simples, escrita no assistente de provas Lean [1]. Ao longo de 24 dias, seus engenheiros e matemáticos dirigiram enxames de dezenas de agentes de IA que produziram cerca de 43,1 milhões de linhas de código Lean [1][2].

O que a Axiom formalizou?

A classificação, frequentemente chamada de teorema enorme, lista os blocos de construção de todos os grupos finitos, a matemática da simetria [1]. Ela diz que todo grupo finito simples é cíclico de ordem prima, alternante, de tipo de Lie ou um dos 26 grupos esporádicos [2].

A Axiom diz que a prova original tem cerca de 15.000 páginas em mais de 500 artigos de cerca de 100 matemáticos [1]. Sua versão em Lean segue a prova de primeira geração e, de acordo com a página do projeto no GitHub, é sorry-free, ou seja, nenhum passo é deixado sem prova [3].

A Axiom diz que seus agentes de IA produziram cerca de 43,1 milhões de linhas de Lean em 24 dias para formalizar a classificação. O site do projeto lista 2,05 milhões de declarações e 715 artigos e livros no corpus [2]. A Axiom diz que a formalização incorpora cerca de 1,2 milhão de linhas de um projeto anterior, o Qiuzhen-CFSG, e se baseia na biblioteca Mathlib [1].

Como funcionou o enxame de agentes?

A Axiom abriu um canal no Slack para o projeto em 1º de outubro de 2026 e o primeiro enxame entrou em operação em 2 de outubro [1]. Um mapa de prova extraído da literatura dividiu o trabalho em 108 marcos e cerca de 380 tarefas menores, que os agentes reivindicaram por meio de issues no GitHub [1].

Agentes principais decompuseram argumentos difíceis e revisaram afirmações, enquanto outros buscaram resultados existentes ou escreveram provas em Lean [1]. Matemáticos humanos lidaram com obstruções matemáticas e engenheiros mantiveram o sistema funcionando [1]. A Axiom diz que deletou dezenas de milhares de linhas construídas com base em suposições não provadas e reiniciou partes do trabalho [1].

Em 10 de outubro, segundo a Axiom, uma mensagem no canal anunciou que os agentes haviam provado que o grupo Monstro é simples [1]. O Lean verifica as deduções, enquanto humanos inspecionam a afirmação final e as definições para confirmar que expressam o teorema pretendido [1].

Quais erros os agentes de IA encontraram?

A Axiom diz que a maioria dos problemas encontrados foi menor, como erros tipográficos, falhas em tabelas ou hipóteses omitidas [1]. A Axiom encontrou 34 desvios notáveis do registro publicado que precisaram ser resolvidos. O caso mais substancial envolveu o Teorema do Grupo Desequilibrado [1][2].

Lá, os agentes encontraram contraexemplos a uma afirmação de fechamento no argumento de John Walter de 1986, o que deixou um passo-chave sem justificativa sem refutar o teorema em si [1]. Um argumento alternativo baseado na teoria de 1976 de Ronald Solomon sobre 2-componentes maximais tornou-se um novo resultado, escrito em um artigo de 35 páginas [1][2]. Solomon e Richard Lyons, que trabalharam na classificação original, foram consultados [1].

Alguém fora da Axiom verificou a prova?

Ainda não, segundo o RuntimeWire [4]. Carina Hong, CEO da Axiom, disse ao RuntimeWire que nenhum grupo externo ainda reconstruiu e verificou a prova. A Axiom está publicando os artefatos de build para que outros possam reproduzi-la [4].

A página do GitHub diz que um único comando de build verifica todo o projeto, e que a Axiom usou mudanças pendentes no Lake, a ferramenta de build do Lean, para manter o tempo de build abaixo de 24 horas [3]. O AI Pin cobriu as alegações separadas da OpenAI sobre novas descobertas em matemática em 27 de outubro.

Nossa leitura

Opinião: Auditar uma prova que nenhuma pessoa jamais leu por completo é um uso mais convincente de IA em matemática do que perseguir novas manchetes, e encontrar 34 desvios reais mostra que a auditoria teve peso. O resultado é tão forte quanto suas verificações externas, porém, então uma reconstrução independente e uma revisão de errata em teoria de grupos importam mais que a contagem de linhas.

O que não pudemos verificar

• Se a prova de 43,1 milhões de linhas compila e verifica fora da Axiom; segundo o RuntimeWire, nenhum grupo externo havia concluído uma reconstrução até 27 de outubro de 2026.
• Quais modelos de IA alimentaram os agentes; a Axiom apenas diz que usou uma mistura variável de modelos.
• Como teóricos de grupos independentes julgam o resultado; não encontramos reação publicada de um teórico de grupos fora do círculo consultivo da Axiom na publicação.
• A lista completa dos 34 desvios notáveis; a Axiom diz que publicará a lista de errata após consultar teóricos de grupos.
• Se o novo artigo sobre o Teorema do Grupo Desequilibrado se sustenta sob revisão por pares; ele está postado no Hexagon, e não pudemos confirmar nenhuma revisão por pares em jornal.