Axiom Math divulga primeira prova formal verificada por computador da Classificação dos Grupos Simples Finitos

A Axiom Math anunciou a primeira prova completa da Classificação dos Grupos Simples Finitos (CFSG) verificada por computador, em Lean. A prova original tem cerca de 15 mil páginas, mais de 500 artigos e aproximadamente 100 autores. O projeto durou 24 dias, com enxames de dezenas de agentes de IA e cerca de 43,1 milhões de linhas de código. A empresa diz que formalizou a prova de primeira geração, porque a de segunda geração ainda está incompleta.

O trabalho começou em 1º de outubro de 2026, com um canal no Slack, e foi dividido em 108 marcos e cerca de 380 tarefas menores a partir de um mapa de prova interno. Agentes reivindicavam tarefas via GitHub issues e podiam delegar pré-requisitos a outros agentes. Houve retrabalho: marcos que escondiam pré-requisitos enormes, assumidos em vez de provados, levaram à exclusão de dezenas de milhares de linhas. Outro gargalo foi o tempo de build, resolvido com cache distribuído, verificação paralela e certificados para cálculos finitos, o que acelerou a checagem em ordens de grandeza.

A formalização expôs 34 desvios relevantes em relação ao registro publicado, o mais substancial ligado ao Unbalanced Group Theorem, além de erros menores como typos e hipóteses omitidas. A Axiom diz que o trabalho gerou um resultado novo em teoria de grupos e que divulgará a lista de errata com consulta a especialistas.

Em 7 de setembro de 2026, o CEVIU noticiou "Claude da Anthropic Formaliza Teorema de Fermat com Prova Verificada por Computador", feito em 11 dias no Lean. Em 8 de setembro de 2026, o CEVIU publicou "IA da Anthropic Gera Prova do Último Teorema de Fermat, Mas Desafia Adoção Ampla", citando 13 milhões de linhas de código. São empresas e problemas diferentes, mas o caso da Axiom amplia a escala: 43,1 milhões de linhas, 24 dias e um corpo de literatura disperso em centenas de artigos, com coordenação de enxames de agentes.

Para quem trabalha com agentes e verificação formal, a leitura é que o gargalo deixou de ser só gerar provas e passou a ser coordenação, revisão de enunciados e infraestrutura de build. O risco de agentes adicionarem hipóteses que mudam o teorema, descrito pela própria Axiom, é um problema que vale acompanhar em qualquer fluxo com Lean.