IA prova Último Teorema de Fermat em 13 milhões de linhas

O que realmente aconteceu

O autor, Alex Korbonits, começa corrigindo as manchetes: a Anthropic não resolveu o Último Teorema de Fermat - Andrew Wiles o provou em 1994, com Richard Taylor fechando a lacuna. O que aconteceu em 4 de setembro de 2026 foi diferente: uma máquina escreveu uma prova do teorema em Lean, e o kernel do Lean a verificou, gerando um arquivo compilável que termina com o teorema a^n + b^n ≠ c^n.

A prova e suas camadas de verificação

O artefato é público, sob licença Apache-2.0, no repositório anthropics/fermats-last-theorem. O build inclui um #guard_msgs que falha se a prova depender de algo além de três axiomas (propext, Classical.choice, Quot.sound) - não compila se houver sorry ou axioma adicionado. Duas camadas extras: o comparador leanprover/comparator v4.33.0 confirmou que a prova casa com um arquivo de desafio escrito só com Mathlib, e o nanoda, um kernel independente em Rust, aceitou a exportação do ambiente com mais de 1 milhão de declarações sem erros (a Anthropic aplicou quatro correções ao nanoda para que terminasse, dizendo que nenhuma enfraquece regras de tipagem).

Os números: 60.475 módulos, 29.511 teoremas, cerca de 13 milhões de linhas geradas em onze dias, com aproximadamente seis bilhões de tokens de saída de um modelo interno comparado ao Fable 5.1, dezenas de agentes coordenados pela plataforma Prove2Me via um grafo acíclico dirigido de dependências. A própria Anthropic diz que a abordagem totalmente autônoma não funcionou - o DAG foi o que fez funcionar. O autor nota uma imprecisão: em linhas de código, 13 milhões equivale a mais perto de quinze vezes o Mathlib do que as cinco vezes anunciadas.

Por que ninguém precisou confiar na pergunta

A diferença para trabalhos anteriores é que a pergunta não foi escrita pela Anthropic. O enunciado é o mesmo de Fermat em 1637, e sua formalização já existia no Mathlib, escrita por pessoas sem interesse no resultado, anos antes. O crédito, argumenta o autor, não é do modelo, mas de uma década de infraestrutura: Mathlib, o projeto FLT de Kevin Buzzard no Imperial, o flt-regular - o ATTRIBUTION.md lista 106 arquivos adaptados dessas fontes. Onze dias de computação se apoiaram em cerca de dez anos desse trabalho.

A verificação saiu do hardware doméstico

O autor se corrige: em agosto ele afirmou que provas assim eram verificáveis em hardware de consumo em menos de uma hora. Com 13 milhões de linhas isso acabou. O build exige cerca de 5 GB por job paralelo, alguns módulos pedem até 36 GB; a execução da própria Anthropic levou 5h32 com 96 jobs, pico de 153 GB de memória e cerca de 220 GB de arquivos transitórios. O comparador leva cerca de 15 horas com pico de 230 GB (recomendam 300 GB), e a exportação para o nanoda tem 37,8 GB. A verificação continua mecânica - um compile, não um julgamento - e alugar a máquina custa menos que uma passagem de avião, mas o conjunto de quem consegue verificar independentemente voltou a ser pequeno.

O que nenhuma ferramenta verifica

O repositório admite que nenhuma ferramenta confere se cada teorema intermediário significa o que o nome sugere. O PROOF-PATH.md lista os desvios: FreyPackage.Mazur_Frey não prova os teoremas de Mazur sobre isogenias; Langlands–Tunnell aparece só no caso octaédrico; os teoremas de lifting de modularidade valem sob condições específicas de nível. Numa etapa, um agente reprovou a modularidade em vez de usar a hipótese - provou o teorema de Wiles duas vezes porque era mais barato que consultar. O resultado: o enunciado de topo está exatamente certo e verificado de três formas, mas os 29.511 teoremas abaixo têm nomes de pipeline e ninguém os leu. Não se pode citar esses lemas em papers nem importar e construir sobre eles: são 13 milhões de linhas que provam uma coisa, contra as 871 mil do Mathlib que provam milhões citáveis.

O gargalo humano

Kevin Buzzard publicou sua própria análise. Sua revisão consistiu numa auditoria de segurança: inspecionar manualmente tudo que não era definição ou prova para verificar que nada era malicioso - com a partição feita pelo próprio modelo auditado. Ele conclui que nenhuma dessas 13 milhões de linhas pode entrar no Mathlib, que não aceita revisão por IA e tem 3.073 pull requests abertos, sendo a capacidade humana de revisão o gargalo. O maior formal proof da história vale, como contribuição à biblioteca compartilhada, zero linhas - embora complete a lista de 100 teoremas de Wiedijk.

O contraponto manual

O autor trabalha no outro extremo: um leanblueprint para Ricci flow, com 7.304 linhas, 278 declarações e nenhum sorry, mirando o teorema de Hamilton (1982) e, no fim, o de Perelman. Manda PRs pequenos para o Mathlib; um deles, de 29 linhas, está aberto há 21 dias rotulado automaticamente como LLM-generated. A lição: os próximos anos não serão uma briga dramática, mas tudo movendo na velocidade em que as pessoas conseguem ler. A máquina é extraordinária para preencher provas quando outra pessoa escreveu a pergunta - e escrever perguntas ainda é trabalho humano: a Anthropic levou onze dias porque Buzzard e o Mathlib gastaram dez anos escrevendo as perguntas.

O autor encerra com uma ressalva de honestidade: ele não executou o build, o comparador nem o nanoda por falta de hardware, então suas afirmações sobre correção se baseiam no que a Anthropic reporta, não em verificação própria. O texto foi escrito com Claude, com o mesmo aviso de sempre: não confie nele, e não confie no autor.