Fermat em Lean: o que a prova verificada por IA muda

Em 4 de setembro de 2026, a Anthropic publicou que agentes do Claude concluíram uma prova do Último Teorema de Fermat inteiramente verificada por computador, escrita na linguagem Lean. A execução durou 11 dias, entre 7 e 17 de agosto de 2026, e produziu cerca de 13 milhões de linhas de código. O que a máquina fez, e vale deixar claro na primeira linha, não foi inventar matemática nova: foi traduzir uma prova já conhecida desde 1995 para um formato em que o computador confere cada passo sozinho.

Ilustração de quadro-negro escolar — Imagem: rawpixel (CC0)

A distinção parece sutil e não é. Ela separa a manchete exagerada do fato técnico que importa: a etapa mais lenta da matemática formalizada, escrever a tradução linha a linha, deixou de ser o gargalo. O gargalo virou a revisão.

Assistente de provas, Lean e Mathlib: o vocabulário básico

Um assistente de provas é um programa que oferece uma linguagem para definir objetos matemáticos, enunciar propriedades sobre eles e demonstrar que essas propriedades valem. A definição é da própria comunidade Lean. A ideia central: o software não acredita em nada por autoridade. Cada passo precisa se reduzir aos axiomas e às regras de inferência que o núcleo do sistema aceita. Se o argumento tem buraco, não compila.

Lean é um desses assistentes, desenvolvido principalmente por Leonardo de Moura e hoje mantido pela Lean FRO. Ele é ao mesmo tempo linguagem de programação e verificador. Mathlib é a biblioteca matemática construída sobre o Lean por uma comunidade aberta, e é ela que torna projetos grandes viáveis: sem uma base pronta de teoria dos anéis, topologia e análise, cada prova começaria do zero. As estatísticas públicas do projeto registram 136.786 definições, 287.530 teoremas e 772 pessoas que já contribuíram.

Traduzir não é descobrir

O Último Teorema de Fermat foi demonstrado por Andrew Wiles em 1995, num artigo de 129 páginas. A prova é aceita há três décadas. O que faltava era a versão formal, legível por máquina, e ela era o último item em aberto da lista de 100 problemas de verificação formal organizada por Freek Wiedijk.

A formalização feita pelo Claude seguiu uma versão simplificada do argumento de Wiles, na exposição de Darmon, Diamond e Taylor. Ou seja: o roteiro matemático já existia e foi escolhido por humanos. A própria Anthropic marca a diferença, contrastando esse trabalho com pesquisas recentes de IA que geraram matemática nova e afirmando que aqui o que é inédito é a verificação, não o resultado. Kevin Buzzard, professor de matemática pura no Imperial College London, foi ainda mais direto ao dizer que a formalização “just faithfully follows the early literature on the proof and adds nothing”.

O projeto do Imperial College existia bem antes da IA

Em 30 de abril de 2024, Buzzard anunciou no blog da comunidade Lean o início de um projeto para formalizar o Último Teorema de Fermat, financiado pelo EPSRC britânico por cinco anos. Ele registrou em seu blog que recebeu “£1M to run my project over 5 years”. O objetivo declarado não era chegar ao fim de uma vez: era reduzir o teorema a resultados que já eram conhecidos pelos matemáticos no fim dos anos 1980, por um caminho moderno.

O método é humano e incremental. O projeto usa o software de blueprint de Patrick Massot, que transforma a prova num mapa de dependências com documentação em LaTeX, quebrando o argumento em lemas pequenos o bastante para serem distribuídos entre colaboradores. Esse trabalho não foi desperdiçado pelo feito da Anthropic: o relatório técnico da empresa registra que 106 arquivos do projeto do Imperial College foram adaptados, além de material do projeto flt-regular.

Os números do feito

11 dias de execução, de 7 a 17 de agosto de 2026, com anúncio público em 4 de setembro de 2026.
Cerca de 13 milhões de linhas de Lean, sendo aproximadamente 10,5 milhões fora o boilerplate gerado automaticamente.
60.474 arquivos, quase todos escritos por máquina.
30.300 teoremas intermediários provados, dos quais cerca de 29.500 entraram na prova final (29.511 na árvore de dependências, segundo o relatório técnico).
Aproximadamente 6 bilhões de tokens de saída. O The Next Web estimou o custo em torno de 300 mil dólares pelos preços de tabela.
Mais de cinco vezes o tamanho da Mathlib inteira.
Tentativas fracassadas do Claude contribuíram com cerca de 7% das linhas não triviais da prova final.

O esforço foi liderado por Tianyi Peng, pesquisador da Anthropic cujo grupo na Universidade Columbia desenvolveu a plataforma Prove2Me usada na execução. Buzzard revisou o resultado e não encontrou trapaça nem exploração de falhas de solidez do sistema.

As limitações que a própria Anthropic lista

O relatório técnico da empresa é incomumente franco sobre os defeitos do que foi produzido. Vale ler a lista antes de qualquer entusiasmo:

Os teoremas nomeados no código como “Ribet”, “Wiles”, “Mazur” e “Langlands-Tunnell” são versões restritas, e o documento avisa que nenhum deles deve ser citado como formalização do teorema clássico geral.
O código não é legível como matemática. Foi publicado sem comentários e sem a docstring por definição que a Mathlib exige.
Há redundância pesada: cerca de dois em cada cinco enunciados de teorema repetem, palavra por palavra, algo já dito em outro arquivo.
É frágil a mudanças de versão. Uma atualização do Lean 4.30 para o 4.33 alterou 7.620 dos 29.511 arquivos de prova (26%), e 5.672 deles (19%) precisaram de conserto individual.
A verificação por máquina reduz o risco, mas não o elimina: a confiança depende do núcleo do Lean, que também é software.

Como a comunidade matemática reagiu

A reação dominante foi de interesse pelo processo, não pelo resultado. Buzzard publicou em 4 de setembro de 2026 um texto com o título “FLT: Anthropic has beaten me to it” e resumiu assim: “mathematically this work of anthropic tells us essentially nothing”. A comunidade de teoria dos números já considerava a prova de Wiles correta com quase total certeza, então confirmá-la não muda o mapa da disciplina.

O que impressionou foi a viabilidade da autoformalização em escala. Ao mesmo tempo, apareceu um problema social concreto: nada dessas 13 milhões de linhas entra na Mathlib como está. A biblioteca depende de revisão humana, já convive com um acúmulo de milhares de pull requests em aberto, e revisores têm resistência a auditar código gerado por IA. O próprio Buzzard observou que o repositório “takes nearly 20 times as long to compile as Lean’s mathematics library”. O gargalo migrou de escrever para revisar.

O que muda na prática, inclusive para quem escreve software crítico

Para a matemática, o efeito de curto prazo é modesto e o de médio prazo pode ser grande. Buzzard sustenta que seu projeto financiado continua fazendo sentido porque ele prometeu ao EPSRC coisas que a formalização da Anthropic não entrega: contribuições permanentes para a Mathlib e um documento navegável que permita a humanos entender a prova moderna. A aposta dele é que passemos a ver “formalization of modern research being done on the fly”, com máquinas apontando lacunas em argumentos antes que eles sejam publicados.

Para quem escreve software crítico, a leitura é mais imediata, porque Lean já é usado fora da matemática. O site oficial da linguagem lista casos como a verificação do Cedar, sistema de autorização da AWS, a biblioteca ArkLib para provas criptográficas do tipo SNARK, o projeto Veil para protocolos distribuídos e o Aeneas, que liga Rust a Lean para os casos em que a segurança de memória do Rust não basta. O padrão prático que emerge do caso Fermat é este:

A especificação continua sendo trabalho humano. Se o enunciado formal estiver errado, a prova verificada certifica a coisa errada com perfeição.
A prova em si vira commodity. Preencher milhares de passos intermediários é exatamente o tipo de tarefa em que agentes com verificador acoplado funcionam bem, porque o compilador dá o sinal de certo ou errado sem ambiguidade.
Manutenção é o custo escondido. Um salto de versão do Lean quebrou um quarto dos arquivos do projeto. Código verificado ilegível e sem documentação é dívida técnica, não patrimônio.
Revisão semântica não desaparece. Alguém precisa confirmar que os teoremas formalizados dizem o que você acha que dizem, e essa capacidade humana passou a ser o recurso escasso.

Resumindo sem exagero: em agosto de 2026 uma máquina não descobriu nada sobre Fermat. Ela mostrou que traduzir matemática de fronteira para uma forma que o computador confere sozinho ficou muito mais barato e rápido, e que o problema seguinte é organizacional.