A Axiom Math, uma empresa sediada em São Francisco que desenvolve sistemas de IA para matemática, lançou a primeira prova completa verificada por computador da Classificação de Grupos Finitos Simples (CFSG), amplamente descrita como a prova mais longa da história da matemática. De acordo com o anúncio da empresa, engenheiros e matemáticos dirigiram enxames de dezenas de agentes de IA durante apenas 24 dias para produzir aproximadamente 43,1 milhões de linhas de código no assistente de prova Lean, verificando um resultado que anteriormente abrangia cerca de 15.000 páginas em mais de 500 artigos de periódicos escritos por cerca de 100 matemáticos ao longo de várias décadas.
A conquista surge num momento em que a matemática assistida por máquinas está a acelerar rapidamente e os meios de comunicação que acompanham notícias de investigação em IA observaram a verificação formal passar de uma prática de nicho para uma capacidade de fronteira. O que torna este lançamento incomum é a escala: a formalização contém cerca de 2,05 milhões de declarações organizadas em 100 marcos, cada um deles verificado pelo kernel do Lean, o pequeno núcleo confiável que verifica cada passo lógico.
O que a classificação realmente diz
Grupos finitos simples são os blocos de construção indivisíveis da simetria finita, e a classificação - apelidada de "teorema enorme" - fornece uma lista completa deles. De acordo com a documentação do projeto, cada grupo finito simples é um de quatro tipos: um grupo cíclico de ordem primária, um grupo alternado em pelo menos cinco símbolos, uma das dezesseis famílias infinitas de grupos do tipo Lie construídos sobre corpos finitos, ou um dos exatamente 26 grupos esporádicos que não se enquadram em nenhuma família.
Provar que esta lista esgota todas as possibilidades exigiu quase um século de esforço coletivo. John Thompson, cujo trabalho foi fundamental para a classificação, recebeu a Medalha Fields em 1970 e o Prémio Abel em 2008. A prova foi tão longa e tão distribuída entre artigos e gerações de matemáticos que dúvidas persistentes sobre a sua completude persistiram durante décadas – dúvidas que esta formalização agora dissipa formalmente.
Enxames de agentes em 500 fontes
A prova original está espalhada por mais de 500 artigos e livros, muitos escritos há décadas em notações incompatíveis. Um engenheiro da Axiom descreveu o método na discussão do lançamento no Hacker News: um enxame de agentes foi encarregado de passar por todas essas fontes, sendo a parte difícil reunir tudo em um todo coerente, já que o mesmo conceito informal pode ser formalizado de maneiras ligeiramente diferentes, mas matematicamente incompatíveis.
A postagem no blog da empresa afirma que o esforço levou 24 dias desde o início até o lançamento, com engenheiros humanos e matemáticos conduzindo os enxames de agentes em vez de trabalhar linha por linha. O resultado segue marcos anteriores de autoformalização de alto perfil em 2026, incluindo provas Lean dos principais teoremas clássicos produzidos com modelos de fronteira, mas em uma escala que nenhum projeto anterior se aproximou.
34 Desvios do registro publicado
A tradução da prova publicada para um formato verificável por máquina expôs problemas reais na literatura matemática. A Axiom relata que a maioria dos problemas eram menores – erros tipográficos, erros em tabelas ou hipóteses descartadas. Mas houve 34 desvios dignos de nota em relação ao registo publicado que precisavam de ser resolvidos antes da formalização ser concretizada.
O mais substancial dizia respeito ao Teorema do Grupo Desequilibrado. Ao formalizar uma rota de primeira geração para o resultado, a equipe encontrou contra-exemplos para uma afirmação de fechamento usada em um argumento publicado. Em consulta com teóricos de grupos especialistas, eles construíram uma rota alternativa baseada nas técnicas estruturais da era Daniel Gorenstein – especificamente a teoria dos 2 componentes máximos da década de 1970 – e publicaram a correção como um novo artigo de teoria de grupo de 35 páginas, publicado como pré-impressão 2610.00575. A empresa afirma que divulgará uma longa lista de erratas para o benefício da comunidade matemática, compilada em consulta com os teóricos do grupo em cujo trabalho se baseia a classificação.
Por que a matemática verificada por máquina é importante
O valor de uma formalização não é apenas o fato de um computador ter aprovado a prova. Uma formalização Lean reduz a base de confiança ao kernel do assistente de prova — um programa pequeno e altamente auditado — em vez da confiança acumulada de milhares de páginas lidas por especialistas dispersos. Os comentadores do tópico Hacker News, onde a história atraiu centenas de votos positivos, notaram que o conhecimento empírico sobre a razão pela qual a classificação se mantém corria o risco de literalmente desaparecer à medida que a geração original de matemáticos se reformasse, porque nenhuma pessoa conseguia manter todo o argumento na sua cabeça.
Existem ecos práticos em outras partes da física também. O maior dos 26 grupos esporádicos, o grupo Monster, aparece no programa "monstruoso luar" conectando simetria finita a funções modulares - trabalho que rendeu a Richard Borcherds a Medalha Fields em 1998 - e na proposta de Edward Witten de 2007 ligando as simetrias do Monstro à entropia do buraco negro em um universo tridimensional simplificado. Uma classificação verificada coloca a matemática estrutural subjacente em terreno mais firme exatamente para esses tipos de aplicações interdisciplinares.
O que vem a seguir
Axiom diz que mais artigos derivados da formalização estão a caminho, juntamente com o projeto de errata. Para a comunidade de métodos formais, o lançamento estabelece uma nova referência para o que os projetos de verificação dirigida por agentes podem tentar; para a matemática, converte uma extensa conquista colaborativa de meio século em um único artefato que qualquer computador pode verificar. A classificação não é mais apenas acreditada. Agora está, no sentido mais literal, comprovado – e a prova está disponível para qualquer pessoa baixar e verificar.
