Claude formaliza teorema de Fermat em 11 dias

A Anthropic anunciou em 5 de setembro de 2026 que o Claude produziu a primeira formalização completa e verificada por computador do Último Teorema de Fermat, escrita na linguagem Lean. O trabalho levou 11 dias e foi conduzido de forma majoritariamente autônoma por um modelo interno de pesquisa da empresa.

Os números do processo são a parte mais concreta do anúncio. A execução gerou cerca de 13 milhões de linhas de código Lean, demonstrou 30,3 mil teoremas — dos quais aproximadamente 29,5 mil são resultados intermediários usados para sustentar a prova final — e consumiu cerca de 6 bilhões de tokens de saída.

O teorema, enunciado por Pierre de Fermat no século 17, só foi provado por Andrew Wiles em 1995. A formalização feita pelo Claude segue uma versão simplificada dessa demonstração, atribuída aos matemáticos Darmon, Diamond e Taylor.

O que “formalizar” significa aqui

Formalizar não é descobrir uma prova nova. É reescrever uma demonstração já aceita em uma linguagem que um verificador automático consegue conferir linha a linha, sem depender da leitura humana. A comunidade matemática estimava que traduzir a prova de Wiles para Lean levaria vários anos de esforço coletivo.

O artefato final é grande: roda em torno de cinco vezes o tamanho da Mathlib, a biblioteca comunitária de matemática formalizada sobre a qual a prova foi construída. A própria Anthropic reconhece que a prova do Claude é provavelmente muito mais longa do que precisaria ser, e menos concisa do que o padrão da Mathlib.

A plataforma que segurou o projeto

O resultado depende tanto do modelo quanto da infraestrutura de coordenação. O trabalho foi montado sobre o Prove2Me, plataforma colaborativa aberta para formalização de matemática projetada por Tianyi Peng e colaboradores na Universidade Columbia.

O Prove2Me mantém um grafo acíclico dirigido com os enunciados dos teoremas e suas dependências, separa enunciado de demonstração para otimizar a compilação em Lean e permite descrever teoremas em linguagem natural, o que facilita reaproveitamento e busca. É o que permite vários agentes Claude trabalharem contra a mesma árvore de dependências sem se atropelarem.

As tentativas anteriores, sem esse arranjo, fracassaram justamente por aí: segundo a empresa, múltiplos agentes perdiam o rastro do estado do projeto e paravam de colaborar de forma eficaz, contribuindo com apenas cerca de 7% do código não trivial.

Por que isso importa fora da matemática

A leitura de fundo é sobre verificação. Se autoformalização em escala funciona, revisões de artigos que hoje consomem anos podem encolher, e erros em demonstrações já publicadas passam a ser detectáveis por máquina. Para a indústria de IA, é também uma das poucas tarefas em que o acerto do modelo é checável de forma objetiva — o compilador aceita ou rejeita.

Fontes: Anthropic · SiliconANGLE