Axiom diz que enxames de agentes de IA verificaram por computador a prova mais longa da matemática — a classificação dos grupos simples finitos — em 24 dias

A startup de IA Axiom afirma ter produzido a primeira prova completa verificada por computador da Classificação dos Grupos Simples Finitos (CFSG) — o resultado que lista todos os «átomos» da simetria finita e cuja prova humana original ocupa cerca de 15.000 páginas em mais de 500 artigos de uns 100 matemáticos.

Como foi feito

Segundo o relatório da Axiom de 26 de outubro, engenheiros e matemáticos dirigiram enxames de dezenas de agentes de IA durante 24 dias (a partir de 1–2 de outubro de 2026), produzindo cerca de 43,1 milhões de linhas de código no assistente de provas Lean, que verifica cada passo lógico. O trabalho seguiu a prova de «primeira geração», apoiou-se no Mathlib e foi dividido em 108 marcos e cerca de 380 tarefas. Entre outras coisas, os agentes provaram que o grupo Monstro é simples.

O que as máquinas encontraram

A maioria dos problemas encontrados na literatura era menor (erros de digitação, erros em tabelas, hipóteses omitidas), mas a Axiom relata 34 desvios notáveis do registro publicado. O maior diz respeito ao Teorema do Grupo Desbalanceado: os agentes acharam contraexemplos a um passo do argumento de John Walter de 1986, e a equipe construiu uma rota alternativa, incluindo um resultado novo estabelecido por seu provador, após consultar os teóricos de grupos Richard Lyons e Ronald Solomon. A Axiom promete publicar uma lista de erratas.

Ressalvas

O Lean verifica as deduções, mas humanos ainda precisam confirmar que os enunciados e definições formais capturam de fato o teorema pretendido. Segundo reportagens de 27 de outubro, nenhum grupo externo havia reconstruído de forma independente a prova completa; a Axiom publicou o repositório e os artefatos de compilação para permitir isso. As afirmações vêm do próprio relatório da empresa.