Axiom Math lança prova Lean da classificação dos grupos com 43,1 milhões de linhas

Em 27 de outubro de 2026, a Axiom Math anunciou que está lançando o que chama de primeira prova completa, verificada por computador, da Classificação dos Grupos Simples Finitos. Produzida ao longo de 24 dias por engenheiros e matemáticos que coordenaram enxames de dezenas de agentes de IA, a prova foi escrita no assistente de provas Lean e tem aproximadamente 43,1 milhões de linhas de código.

“Hoje, estamos lançando a primeira prova completa, verificada por computador, da Classificação dos Grupos Simples Finitos (CFSG)”, escreveu a empresa em seu anúncio. A classificação identifica os blocos de construção básicos dos grupos finitos, e sua prova original se estende por cerca de 15 mil páginas, em mais de 500 artigos de aproximadamente 100 matemáticos — uma escala que lhe rendeu o apelido de teorema gigantesco.

O que a Axiom lançou

A CFSG estabelece que todo grupo simples finito é cíclico de ordem prima, alternado sobre pelo menos cinco símbolos, pertence a uma de dezesseis famílias infinitas de grupos de tipo de Lie construídos sobre corpos finitos ou é um dos exatamente 26 grupos esporádicos isolados; o anúncio observa que alguns autores contam o grupo de Tits como um 27º grupo. O maior grupo esporádico, o Monstro, foi construído por Robert Griess em 1980 com uma álgebra de dimensão 196.884.

O esforço humano para provar o teorema se estendeu por décadas. Em 1963, Walter Feit e John Thompson provaram que todo grupo simples finito não abeliano tem ordem par, em um artigo de 255 páginas que ocupou uma edição inteira do Pacific Journal of Mathematics. Daniel Gorenstein delineou, em 1972, um programa de dezesseis etapas para concluir a classificação e declarou-a completa em 1983, mas o caso quase fino dependia de um manuscrito inacabado de Geoffrey Mason até que Michael Aschbacher e Stephen Smith publicaram, em 2004, um tratamento de 1.221 páginas, encerrando o que ficou conhecido como a prova de primeira geração. Uma prova de segunda geração, mais sistemática, iniciada por Gorenstein e Richard Lyons e posteriormente com a participação de Ronald Solomon e Inna Capdeboscq, continua incompleta; por isso, a Axiom formalizou a prova de primeira geração.

A página do projeto apresenta a formalização como uma versão da prova de primeira geração em que cada etapa lógica é verificada pelo núcleo do Lean e informa que ela contém 43,1 milhões de linhas de Lean, 2,05 milhões de declarações e um corpus de 715 artigos e livros. A Axiom afirma que seu mapa da prova se baseou nos volumes da prova de segunda geração e que a formalização incorpora cerca de 1,2 milhão de linhas de código do projeto anterior Qiuzhen-CFSG, além de se apoiar no Mathlib, cuja criação atribui a centenas de colaboradores. O projeto identifica Dean Cureton, Vasily Ilin, Bhavik Mehta e Niels Voss como colaboradores principais, e Letong Hong como investigador principal.

O repositório público no GitHub descreve o resultado como uma prova em Lean4 sem uso de sorry, fixada na versão 4.35.0-rc3, baseada no Mathlib e no projeto TauCeti e que usa apenas os axiomas padrão Classical.choice, propext e Quot.sound, sem native_decide. Sua formulação formal da classificação, extraída do TauCeti, diz: “Todo grupo simples finito é isomorfo a um dos grupos construídos explicitamente na lista de classificação.” O README informa que lake build verifica todo o desenvolvimento e que alterações ainda em aberto na ferramenta de compilação Lake, junto com otimizações que a equipe planeja incorporar ao projeto principal, reduziram o tempo de compilação para menos de 24 horas; o código está sob a licença Apache-2.0.

Um esforço coletivo de 24 dias

Em 1º de outubro de 2026, a Axiom abriu um canal no Slack para coordenar o projeto. Trabalhos prévios em Lean e um mapa interno da prova, elaborado a partir da literatura publicada, dividiram o esforço em 108 marcos e cerca de 380 tarefas menores; o primeiro enxame entrou em operação em 2 de outubro de 2026, com agentes assumindo marcos por meio de issues no GitHub e informando a conclusão do trabalho no Slack. Os agentes líderes decompunham argumentos difíceis e revisavam enunciados, enquanto outros agentes buscavam resultados existentes ou escreviam provas em Lean. Um agente também podia delegar a outros agentes a busca por pré-requisitos ausentes, e os resultados eram incorporados a um repositório compartilhado.

O progresso inicial revelou pontos fracos. Alguns marcos que pareciam administráveis escondiam pré-requisitos enormes que os agentes haviam presumido, em vez de provar, e a equipe apagou dezenas de milhares de linhas construídas com base nessas suposições antes de recomeçar com um plano mais sólido; um dos primeiros marcos dizia respeito ao teorema do funtor de sinalizador, cuja prova candidata dependia de suposições estruturais que ainda precisavam ser justificadas. O tempo de compilação também se tornou um gargalo, pois os agentes produziam provas mais rápido do que o Lean conseguia verificá-las novamente. A Axiom afirma que seus engenheiros distribuíram entre os trabalhadores os resultados de compilação armazenados em cache, executaram verificações independentes em paralelo e transferiram cálculos finitos dispendiosos para certificados verificáveis separadamente — mudanças que, segundo a empresa, aceleraram a verificação em várias ordens de magnitude.

Em 10 de outubro de 2026, uma mensagem no canal anunciou que os agentes haviam provado que o Monstro é simples, relata a empresa; os agentes também formalizaram a existência do Monstro por meio da álgebra de Griess e um teorema que identifica grupos do tipo Monstro com o próprio Monstro. Em 13 de outubro de 2026, apenas um marco foi concluído, e os engenheiros organizaram um esforço de replanejamento que dividiu os marcos inacabados em teoremas menores e formulados com precisão. Cada decomposição precisava mostrar como as partes estabeleceriam o marco original por meio de uma prova curta em Lean.

Lacunas encontradas na prova publicada

A tradução da demonstração para Lean revelou problemas nos argumentos publicados, informa a Axiom. A maioria era pequena — erros tipográficos, erros em tabelas ou hipóteses omitidas —, mas a empresa contabiliza 34 divergências relevantes em relação ao material publicado, sendo a mais substancial relacionada ao Teorema do Grupo Desbalanceado, ou UGT.

Um exemplo surgiu nos volumes de Aschbacher e Smith sobre grupos quase finos, em que um lema afirmava que duas quantidades numéricas eram iguais. Os agentes encontraram um contraexemplo envolvendo o grupo SL₂(5), no qual uma das quantidades era 1, embora a igualdade afirmada exigisse que fosse 2. Substituir a igualdade por uma desigualdade corrigiu o lema, mas argumentos posteriores haviam usado a igualdade para descartar casos; por isso, a equipe ampliou um argumento anterior para abranger essas configurações.

O UGT ajuda a identificar um grupo inteiro a partir de informações sobre seus subgrupos: de acordo com o resumo de do artigo que acompanha o trabalho, sob as hipóteses indutivas da classificação, a existência de um subgrupo não trivial de ordem ímpar, normal no centralizador de uma involução, implica que o grupo simples ambiente seja de tipo de Lie em característica ímpar ou alternado de determinados graus. A Axiom abordou o UGT por meio das memórias de John Walter, de 1986, e, ao formalizar esse argumento, seus agentes encontraram contraexemplos explícitos a uma afirmação de fechamento nele utilizada: uma operação que, supostamente, manteria os grupos simples associados dentro de uma família especificada podia produzir um grupo explicitamente excluído dessa família.

Segundo o relato da empresa, partindo de PSL₂(49), cuja involução de corpo tem como centralizador PGL₂(7), a operação produz a componente simples PSL₂(7), excluída da família por 7 ser um primo de Mersenne. A Axiom observa que os contraexemplos não refutavam o próprio UGT, nem mesmo a conclusão da Proposição II.5.9(ii) de Walter.

A correção se apoiou na teoria dos 2-componentes maximais de Solomon, de 1976, que, segundo a Axiom, forneceu as ideias centrais para um argumento alternativo produzido e formalizado pelo sistema AxiomProver. A etapa principal, enunciada no artigo como Teorema 2.3 (preservação dos topos simples), é descrita pela Axiom como um novo resultado em teoria dos grupos, demonstrado pelo AxiomProver; combinada com as reduções de Gilman e Solomon e com os teoremas de reconhecimento de Foote e Harris, ela fornece a forma do UGT para grupos simples necessária à classificação. Após a formalização, os matemáticos da Axiom encontraram uma dedução mais curta, baseada em métodos de primeira geração e registrada como Observação 9.5, que chega à mesma conclusão sem o Teorema 2.3.

Esse artigo, The Unbalanced Group Theorem, de Colin Defant e Ken Ono, foi publicado no servidor de preprints Hexagon como versão 1 em 27 de outubro de 2026, sob a licença CC BY 4.0; a página do projeto informa que o artigo tem 35 páginas. A Axiom afirma que está trabalhando com especialistas em teoria dos grupos para compilar as erratas encontradas na literatura e que as publicará na página de erratas do projeto. Lyons e Solomon, cujo trabalho fundamenta a classificação, foram consultados sobre a correção do UGT, e a empresa afirma que continuará compilando e resolvendo as erratas com um conselho consultivo que os inclui, além do consultor externo Dan Nakano. A Axiom apresenta sua contribuição como tornar a demonstração verificável mecanicamente, documentar os obstáculos encontrados e fornecer argumentos formalizados para resolvê-los, ao mesmo tempo que afirma que a classificação continua sendo uma realização dos matemáticos que descobriram os grupos e desenvolveram os argumentos.