A Axiom Math, uma startup que desenvolve sistemas de IA para matemática, garante ter transformado uma das provas mais longas alguma vez escritas em código que um computador consegue verificar passo a passo. Num texto datado de 26 de outubro e num repositório público no GitHub anunciado a 27, a empresa apresentou uma formalização em Lean 4 da Classificação dos Grupos Simples Finitos (CFSG), conhecida como o teorema enorme, e atribuiu a maior parte do trabalho a enxames dos seus agentes AxiomProver, dirigidos por engenheiros e matemáticos.
A classificação estabelece que todo o grupo simples finito é cíclico de ordem prima, alternado, pertence a uma das famílias de tipo Lie ou é um dos 26 grupos esporádicos, o maior dos quais é o Monster. Estes grupos funcionam como as peças elementares de todos os grupos finitos. A demonstração humana está dispersa por cerca de 15 000 páginas em mais de 500 artigos de uma centena de autores, foi dada como concluída em 1983 e só ficou fechada em 2004, com um tratamento de 1221 páginas do caso dos grupos quasithin.
Segundo a Axiom, o projeto durou 24 dias. A 1 de outubro foi aberto um canal de coordenação e construído, a partir da literatura, um mapa da prova com 108 etapas e perto de 380 tarefas; os agentes reclamavam trabalho, delegavam pré-requisitos em falta e enviavam resultados para um repositório comum. Agentes coordenadores decompunham os argumentos difíceis e revisavam os enunciados, enquanto outros procuravam resultados existentes e escreviam Lean. O total chegou a cerca de 43,1 milhões de linhas e, segundo o site do projeto, 2,05 milhões de declarações. A Axiom não revelou que modelos de IA usou.
De acordo com o README, o desenvolvimento não contém sorry, usa o Lean v4.35.0-rc3, assenta no Mathlib e no projeto TauCeti, de onde vem o enunciado da classificação, e recorre apenas aos axiomas padrão, sem native_decide. Aproveita ainda cerca de 1,2 milhões de linhas do esforço Qiuzhen-CFSG. A compilação completa levou quase um dia, mesmo com alterações ainda não publicadas à ferramenta Lake. O código está sob licença Apache 2.0.
O resultado mais curioso talvez seja o que os agentes descobriram pelo caminho. A Axiom aponta 34 desvios relevantes em relação aos textos publicados, na maioria pequenos erros, mas incluindo contraexemplos a um passo de fecho no caminho de John Walter, de 1986, para o Unbalanced Group Theorem. A empresa sublinha que o teorema em si não está em causa. Para tapar a lacuna, o AxiomProver demonstrou um novo resultado de preservação apoiado na teoria das 2-componentes maximais de Ronald Solomon, de 1976, descrito num artigo próprio; mais tarde, matemáticos da Axiom encontraram um argumento mais curto. Os especialistas Richard Lyons e Ronald Solomon aconselharam o projeto e vão ajudar a organizar uma lista de erratas que ainda não foi publicada.
Como termo de comparação, o teorema de Feit-Thompson, com 255 páginas e apenas uma das peças da classificação, exigiu seis anos a uma equipa liderada por Georges Gonthier para ser formalizado em Coq, trabalho concluído em 2012. A Axiom apresenta o novo projeto como continuação dessa tradição e do Mathlib, e não como substituto dos matemáticos que construíram a prova original.
Observadores independentes pedem prudência. O Neural Brew, num artigo de 27 de outubro, escreveu que não havia ainda revisão independente completa e que não conseguira confirmar que a prova volta a compilar. Yoseph Franco, do Arncof, não encontrou qualquer recompilação externa nem posição dos responsáveis pelo Lean ou pelo Mathlib, notou que a publicação da Axiom no X falava em 50 milhões de linhas e centenas de erratas, contra os 43,1 milhões e os 34 desvios do blogue, e lembrou que muitas das reações entusiastas vinham de pessoas ligadas à empresa. O Lean confirma cada dedução, mas cabe a humanos verificar se o enunciado formal traduz de facto a classificação, uma revisão que a própria Axiom pediu aos especialistas em teoria de grupos e à comunidade Lean.