Axiom Math formaliza o “Teorema Enorme” em 43,1 milhões de linhas de Lean em 24 dias

A Axiom Math anunciou a conclusão da verificação por computador do teorema de classificação dos grupos simples finitos (CFSG), que os matemáticos chamam de “Teorema Enorme”. Em 24 dias, dezenas de agentes de IA escreveram cerca de 43,1 milhões de linhas de código em Lean e formalizaram uma demonstração que ocupa 15 000 páginas em mais de 500 artigos científicos. Cerca de 100 pesquisadores trabalharam nela por décadas. A Axiom afirma que este é o primeiro resultado completo do CFSG que pode ser verificado por computador. O código e os materiais foram publicados para análise independente.

A tabela periódica das simetrias

O jeito mais simples de entender o que o teorema classifica é pensar em um cubo. Ele pode ser girado de 24 maneiras diferentes e continuar com exatamente a mesma aparência. Essas rotações formam um grupo matemático. O CFSG descreve os “blocos de construção” fundamentais que compõem todos os grupos finitos de simetrias. O resultado é uma espécie de tabela periódica das simetrias, usada em álgebra, teoria dos números e física matemática.

O problema está na forma como a demonstração foi construída. Ela foi montada aos pedaços, em centenas de artigos, por autores diferentes e em décadas diferentes. Para uma pessoa, revisar tudo isso é praticamente impossível: seria preciso manter na cabeça milhares de lemas interligados e espalhados por revistas científicas. A formalização em Lean resolve esse obstáculo. Cada passo do raciocínio é escrito como código, e o núcleo do Lean verifica mecanicamente que a conclusão decorre dos passos anteriores.

A conta do projeto: 43 milhões de linhas em 24 dias

Os números dão a dimensão do trabalho. São 43,1 milhões de linhas em 24 dias, o que dá cerca de 1,8 milhão de linhas por dia, ou perto de 75 mil por hora, contando o tempo ininterrupto. Cada página da demonstração em papel corresponde a aproximadamente 2 900 linhas de código formal. A formalização é ordens de grandeza mais detalhada que o texto original, porque nos artigos os matemáticos pulam passos “óbvios”, e o Lean não permite isso.

O trabalho foi agêntico, e não uma única geração longa. Dezenas de agentes tocaram ramos de formalização em paralelo, e o código final precisava convergir em uma só demonstração aceita pelo núcleo verificador. É a verificação pelo núcleo que diferencia esse resultado da saída comum de um modelo de linguagem: um passo errado simplesmente não passa.

O que os agentes encontraram pelo caminho

A formalização trouxe não só confirmação, mas também descobertas novas. A Axiom lista os seguintes resultados:

• cerca de 43,1 milhões de linhas de código em Lean, criadas em 24 dias por dezenas de agentes de IA;
• 34 divergências significativas em relação a trabalhos matemáticos publicados;
• contraexemplos para algumas afirmações da literatura e demonstrações alternativas para elas;
• um novo resultado em teoria de grupos, necessário para o caminho de demonstração escolhido;
• em alguns casos, erros encontrados nos raciocínios originais e novos argumentos matemáticos que os corrigem;
• trabalho conjunto com matemáticos, incluindo especialistas que participaram da classificação original.

A participação humana é essencial aqui. Quando a formalização esbarra em uma divergência com a publicação, é preciso um especialista para distinguir um erro de digitação de uma lacuna real. A experiência dos autores da classificação original ajudou a definir onde a versão formal deveria seguir o original e onde era necessário outro caminho.

O que dá para aproveitar na prática

A principal conclusão para a indústria é que agentes que escrevem e verificam o próprio código em um ambiente com verificador rigoroso conseguem lidar com tarefas fora do alcance do trabalho manual. O Lean atua como um juiz que não aceita nada por fé, nem das pessoas nem do modelo. O mesmo esquema vale para qualquer área em que o resultado possa ser checado automaticamente: verificação de software crítico, de protocolos e de construções criptográficas.

Há também uma ressalva importante. A verificação por computador garante que a demonstração está correta em relação às definições e formulações registradas. Por isso, o código aberto importa tanto quanto o resultado em si: os matemáticos poderão ler as definições e confirmar que foi formalizado exatamente o que deveria. A Axiom não informa no anúncio o custo dessa execução (gastos com computação e tokens). É esse número que vai mostrar se a reverificação formal de resultados fundamentais se tornará rotina ou continuará sendo um projeto isolado.

Para os matemáticos, o sinal é claro. A literatura que antes era aceita pela confiança na autoridade agora pode ser reverificada de forma totalmente mecânica, e nesse caminho já apareceram 34 divergências significativas.