IA da Anthropic formaliza o último teorema de Fermat em Lean

A Anthropic publicou uma prova completa e verificada por máquina do último teorema de Fermat, escrita em Lean. A empresa diz que um modelo de investigação interno a gerou em 11 dias. O resultado tem cerca de cinco vezes o tamanho da Mathlib, a principal biblioteca aberta de matemática formalizada.

O Lean é um assistente de prova. Escreve-se matemática como código, e um pequeno programa chamado núcleo verifica cada passo. O último teorema de Fermat diz que não há três inteiros positivos a, b e c que satisfaçam a^n + b^n = c^n quando n é maior do que 2. Andrew Wiles provou-o em 1995. Até agora ninguém tinha escrito essa prova numa forma que um computador conseguisse verificar de ponta a ponta.

O que está mesmo no repositório

O artigo de investigação da Anthropic saiu a 4 de setembro de 2026. O código está no GitHub sob a licença Apache 2.0.

O ficheiro README enuncia o teorema formal. Para inteiros positivos a, b e c, e qualquer n de pelo menos 3, a^n + b^n nunca é igual a c^n.

Item	Valor
Cadeia de ferramentas Lean	4.33.1
Revisão da Mathlib	v4.33.0
Teoremas	29 511
Módulos	60 475
Tempo de compilação	5,5 horas com 96 tarefas em paralelo
Pico de memória	230 GB
Tamanho da exportação	37,8 GB

Duas afirmações do README pesam mais do que o tamanho. A prova não contém nenhum sorry, o marcador do Lean para um passo que ninguém terminou. E assenta em apenas três axiomas: propext, Classical.choice e Quot.sound. Esses três vêm com o próprio Lean. Nada mais foi assumido para fechar o argumento.

A Anthropic diz que o modelo provou 30 300 teoremas no total. Cerca de 29 500 ficaram na prova final. A empresa refere 6 mil milhões de tokens de saída e 13 milhões de linhas de Lean geradas. O trabalho passou pelo Prove2Me, uma plataforma que parte uma formalização em enunciados pequenos e os entrega a agentes a trabalhar em paralelo.

Como a prova foi verificada

Correram três verificações separadas, e esta é a parte que vale a pena perceber.

Primeiro o próprio núcleo do Lean aceitou a prova. Depois uma ferramenta chamada comparator, na versão 4.33.0, voltou a verificá-la em cerca de 15 horas. Por fim o Nanoda, um núcleo independente escrito em Rust, verificou 1 052 234 declarações em cerca de 30 minutos.

O Nanoda conta porque não partilha código com o Lean. Um erro no núcleo do Lean não seria apanhado pelo núcleo do Lean. Uma segunda implementação, noutra linguagem, é um travão real para esse risco.

O que dizem os matemáticos

Kevin Buzzard lidera o Projeto Xena. Tem um financiamento de um milhão de libras do financiador de investigação britânico EPSRC, ao longo de cinco anos, para formalizar exatamente este teorema. Escreveu no seu blogue que a Anthropic lá chegou primeiro.

Buzzard não contesta o resultado. "Tenho 99,9 % de certeza de que a prova do FLT está correta", escreveu. Na página da Anthropic, chama ao trabalho uma "realização extraordinária de autoformalização".

Também traça um limite. A formalização "segue fielmente a literatura inicial sobre a prova e não acrescenta nada", escreveu. Segue a exposição de Darmon, Diamond e Taylor de 1995 sobre o argumento de Wiles. Não se descobriu matemática nova aqui. O que é novo é que a matemática antiga passou a ser verificável por máquina.

Buzzard nota que a prova cobre os primos de pelo menos 17. Os primos irregulares mais pequenos já tinham sido formalizados por outros. Um comentador do seu texto, David Jao, estimou o custo de API da execução em cerca de 300 000 dólares.

O que isto significa para programadores

Se escreve Lean, pode clonar o repositório, mas verifique primeiro o seu equipamento. Uma compilação de 5,5 horas com 96 tarefas, com um pico de 230 GB de memória, exclui quase todos os portáteis. Leia antes a documentação HTML gerada. Tem 390 MB e não precisa de compilação.

A lição transponível não é que um modelo escreveu 13 milhões de linhas. É que ninguém teve de as ler. Um núcleo decidiu se o código estava correto, em minutos, sem confiar naquilo que o produziu.

Isso só funciona onde existe um verificador. O Lean tem um. O seu serviço web não tem. Antes de tomar isto como modelo, pergunte o que faria o papel do núcleo na sua própria pilha. Um sistema de tipos, um teste de propriedades ou um fuzzer são os candidatos habituais.

Se revê Lean escrito por uma IA, duas verificações mecânicas fazem quase todo o trabalho. Procure sorry, e imprima a lista de axiomas. A afirmação da própria Anthropic assenta nesses dois factos, e ambos são baratos de confirmar por si.

A diferença de custo é o último ponto a notar. Produzir a prova levou 11 dias e milhares de milhões de tokens. Voltar a verificá-la noutra linguagem levou meia hora. A Anthropic já apontou modelos de investigação ao trabalho de laboratório, e o mesmo padrão aplica-se aqui. Gerar é caro. Verificar é barato.