Axiom anuncia ter verificado em Lean a classificação dos grupos finitos simples, a prova mais longa da matemática

A start-up Axiom afirma ter tornado verificável por computador a classificação dos grupos finitos simples (frequentemente abreviada CFSG), apelidada de “o teorema enorme”: uma prova de cerca de 15.000 páginas, distribuída em mais de 500 artigos escritos por uma centena de matemáticos ao longo de várias décadas. O anúncio caiu no X nesta terça-feira, 27 de outubro, às 15h34, hora de Paris, acompanhado de um longo artigo de blog datado do dia anterior, de um mapa de prova interativo e de um repositório de código.

Do que se trata

Um grupo descreve simetrias, como as 24 rotações que deixam um cubo inalterado. Os grupos finitos se decompõem em “tijolos” indivisíveis, os grupos simples, um pouco como os números inteiros em números primos. A classificação diz que a lista desses tijolos está completa: grupos cíclicos de ordem prima, grupos alternados (sobre pelo menos cinco elementos), dezesseis famílias infinitas de grupos “de tipo de Lie” e exatamente 26 grupos esporádicos, dos quais o maior, o grupo Monstro. Esse resultado é usado em inúmeras áreas (álgebra, teoria dos números, combinatória), mas pouquíssimas pessoas podem verificar o conjunto.

A Axiom reescreveu essa prova em Lean, um assistente de prova: uma linguagem onde cada definição e cada etapa lógica são escritas com precisão suficiente para que um programa as controle. O site do projeto exibe 43,1 milhões de linhas de Lean e 2,05 milhões de declarações.

Como agentes de IA foram mobilizados

O relato da Axiom é, acima de tudo, o de uma organização. O projeto começa em 1º de outubro de 2026 com um mapa de prova extraído da literatura e do código Lean já existente, dividido em 108 marcos e cerca de 380 tarefas. Já em 2 de outubro, enxames de várias dezenas de agentes AxiomProver, usando uma mistura variável de modelos, solicitam tarefas por meio de tickets GitHub e prestam contas no Slack. Agentes “chefes” dividem os argumentos difíceis e verificam os enunciados; outros buscam resultados existentes ou escrevem as provas.

A Axiom não esconde os contratempos. Marcos aparentemente simples escondiam enormes pré-requisitos que os agentes haviam presumido em vez de demonstrar: dezenas de milhares de linhas foram suprimidas. O tempo de recompilação também se tornou um gargalo, resolvido por um sistema de cache compartilhado entre máquinas. Os humanos permaneceram no centro: matemáticos para os obstáculos de fundo, engenheiros para fazer o sistema funcionar.

O que a máquina encontrou

Formalizar obriga a explicitar o que um leitor humano completa por conta própria. Segundo a Axiom, a maioria dos problemas levantados era menor (erros de digitação, tabelas incorretas, hipóteses esquecidas), mas 34 discrepâncias notáveis com a literatura tiveram de ser resolvidas. A mais séria diz respeito ao teorema dos grupos não equilibrados, na versão de John Walter de 1986: os agentes encontraram contraexemplos para uma etapa do raciocínio, sem, no entanto, refutar o próprio teorema. Com a ajuda de Richard Lyons e Ronald Solomon, dois especialistas históricos da classificação, outra rota foi construída a partir de trabalhos de Solomon de 1976. A Axiom a apresenta como um novo resultado de teoria dos grupos, descrito em um artigo que acompanha a publicação.

A Axiom promete publicar a lista completa de erratas com um comitê de especialistas. Enquanto não estiver on-line, o número total de erros levantados permanece inverificável.

Os limites a ter em mente

O Lean controla as deduções, não o sentido do enunciado: ainda é preciso que humanos verifiquem que o teorema final e suas definições dizem bem o que diz a classificação. A Axiom reconhece isso em seu texto. No momento em que escrevemos, nenhuma verificação independente completa foi publicada e nós não recompilamos nós mesmos o repositório. A formalização também não parte do zero: ela integra cerca de 1,2 milhão de linhas do projeto Qiuzhen-CFSG e se apoia na biblioteca Mathlib.

Esse anúncio chega no dia seguinte aos resultados matemáticos reivindicados pela OpenAI, que apresentamos aqui. A abordagem é diferente: a OpenAI diz ter encontrado resultados novos, a Axiom diz ter verificado mecanicamente um resultado conhecido e ter corrigido trechos dele.