A Axiom, empresa de IA voltada à matemática, anunciou que seu enxame de agentes AxiomProver concluiu em 24 dias a formalização em Lean do teorema de classificação dos grupos simples finitos (CFSG), e afirma que esta é a primeira prova completa do teorema verificada por computador. O código foi aberto no GitHub sob a licença Apache-2.0. O repositório declara que a versão final não tem marcadores sorry, não usa native_decide e depende apenas de três axiomas padrão: extensionalidade proposicional, o axioma da escolha clássico e a solidez dos quocientes.
A classificação dos grupos simples finitos costuma ser chamada de “tabela periódica da simetria”. Ela afirma que todo grupo simples finito pertence a uma de 18 famílias infinitas ou é um dos 26 grupos esporádicos. A prova original está distribuída em mais de 500 artigos, com cerca de 15 mil páginas, escritos por aproximadamente 100 matemáticos entre cerca de 1955 e 2004. A última peça, a parte quasithin de Aschbacher e Smith, ocupa sozinha 1221 páginas.
O que aconteceu nesses 24 dias
Segundo o relato divulgado pela Axiom, o projeto criou o grupo de colaboração no Slack em 1º de outubro, e os primeiros agentes entraram em operação em 2 de outubro. A prova inteira foi dividida em 108 marcos e cerca de 380 pequenas tarefas; os agentes assumiam tarefas por meio de issues no GitHub e relatavam o andamento no Slack. Um agente principal dividia os problemas e revisava os enunciados, enquanto os demais buscavam resultados já existentes ou escreviam provas em Lean, repassando trabalho adiante quando faltavam premissas.
O processo não foi tranquilo. Um lote inicial de código foi apagado por inteiro por causa de erros decorrentes de suposições implícitas, e a equipe replanejou. Mais tarde, a velocidade de compilação virou o gargalo: os engenheiros recorreram a cache e verificação paralela e externalizaram cálculos finitos como certificados verificáveis, reduzindo o build completo para menos de 24 horas. Em 10 de outubro, o projeto anunciou separadamente a prova de que o grupo Monstro é simples.
Quanto ao material de partida, a Axiom diz ter lido 715 artigos e livros no total e reaproveitado cerca de 1,2 milhão de linhas de código do projeto anterior Qiuzhen-CFSG, além de bibliotecas de formalização existentes, como Mathlib e Tau Ceti.
Erros encontrados pelo caminho
Durante a formalização, a equipe registrou 34 desvios matemáticos mais evidentes. O que mais chamou atenção está no caminho do “teorema dos grupos desbalanceados” (UGT): uma afirmação sobre fecho nas memórias de Walter, de 1986, tem contraexemplo, pois partindo de PSL₂(49) chega-se a PSL₂(7), justamente o grupo excluído dessa família. Um lema de Aschbacher e Smith também teve um contraexemplo encontrado, SL₂(5); ao trocar a igualdade por uma desigualdade, o argumento seguinte precisa ser estendido.
A Axiom publicou um artigo próprio de 35 páginas sobre o assunto, propondo um argumento alternativo, e corrigiu esse caminho com a participação de consultores como Lyons e Solomon. A empresa enfatiza repetidamente que esses contraexemplos não refutam o UGT em si, muito menos abalam o teorema de classificação.
“the classification remains the achievement of the mathematicians who discovered the groups”
(A classificação continua sendo a conquista dos matemáticos que descobriram os grupos.)
Em comparação com verificações mecânicas anteriores
Na comparação lateral, a referência mais citada é a verificação do teorema da ordem ímpar concluída em 2012 pela equipe de Gonthier em Coq. Esse teorema vem do artigo de 255 páginas de Feit e Thompson, de 1963; o projeto durou cerca de seis anos e é uma pedra fundamental da prova da classificação. A Axiom cobriu agora o edifício inteiro, e o tempo é contado em dias.
As duas velocidades não são diretamente comparáveis. O projeto da ordem ímpar construiu a biblioteca praticamente do zero, enquanto a Axiom se apoia no Mathlib e nas 1,2 milhão de linhas de código CFSG anteriores; o número de agentes é descrito apenas como “dezenas”, e o poder de computação, o hardware e o custo total por trás não foram divulgados, nem as horas de trabalho humano. Os 24 dias são o ciclo do próprio projeto de formalização, sem contar as décadas de trabalho humano de que ele depende.
Algumas ressalvas também estão claras. Os metadados do projeto marcam a revisão como “autoavaliação”, e até agora nenhum terceiro reproduziu o build completo a partir de um ambiente limpo. A verificação por máquina só garante que a derivação é válida a partir das hipóteses escritas; se as definições do enunciado da classificação são fiéis ao teorema original ainda precisa ser conferido, item por item, por especialistas em teoria de grupos. O artigo sobre o UGT foi publicado em uma plataforma de preprints sem revisão por pares, e a Axiom diz que a lista de errata ficará na página do projeto.
Para quem trabalha com formalização, o próximo passo é observar duas coisas: se a comunidade consegue rodar de forma independente essas 43,1 milhões de linhas e quantos dos 34 desvios serão confirmados pelos autores originais.
Fontes: comunicado do projeto e repositório GitHub da Axiom, Unite.AI, CocoLoop, Kingy AI; número de linhas de código Lean, declarações, marcos e desvios conforme os dados divulgados pela Axiom, duração da verificação do teorema da ordem ímpar conforme materiais da Microsoft Research.