A Anthropic publicou em 4 de setembro uma formalização verificada por máquina do Teorema de Fermat em Lean 4; a API do GitHub situa a criação do repositório em 14:21:04 UTC. A afirmação que circulou foi que Claude provou o Teorema de Fermat em 11 dias. Os próprios arquivos do repositório descrevem algo mais restrito e, em um aspecto, mais interessante.
O que o arquivo de atribuição diz
O repositório traz um ATTRIBUTION.md registrando 106 arquivos que contêm material do projeto FLT do Imperial College London, liderado por Kevin Buzzard, e do projeto flt-regular — "54 em Definitions/, 52 em P2M/Sol/; e os 23 arquivos que reproduzem o texto do Mathlib". Dezenas de linhas dizem "whole file (100%)". O arquivo NOTICE data o empréstimo: "Material was taken from the project's main branch as of 2026-05-21". Na portabilidade da toolchain para Lean 4.33, o arquivo de atribuição registra que ele "left the other 41 byte-identical".
A verificação é real
Nada disso invalida a checagem. O README informa que todos os 60.475 módulos foram compilados, que #print axioms fermat_last_theorem está limitado aos três axiomas padrão e que nenhum módulo contém axiom, sorry, native_decide, unsafe ou partial def. A compilação levou 5 horas e 32 minutos com 96 jobs e teve pico de 153 GB de memória. Os próprios números da Anthropic: 13 milhões de linhas de Lean, 29.500 teoremas intermediários usados na prova final, cerca de seis bilhões de tokens de saída.
O que a narrativa recebida erra
Três coisas. Claude não provou nada novo — trata-se da autoformalização da exposição Darmon–Diamond–Taylor de 1995 do argumento Wiles–Taylor–Wiles, uma prova concluída por humanos há 31 anos. Não foi sem ajuda: pela própria contabilidade da Anthropic, um nono do repositório contém texto Lean humano, parte dele palavra por palavra. E Buzzard, o matemático cuja revisão a Anthropic cita, escreveu no próprio blog no mesmo dia que "mathematically this work of anthropic tells us essentially nothing" e que a formalização "just faithfully follows the early literature on the proof and adds nothing." Vários veículos também chamaram isso de o maior arquivo do gênero; são 60.475 módulos, não um arquivo.
A afirmação honesta ainda é grande
Máquinas agora podem traduzir milhares de páginas da literatura matemática existente para uma forma verificável pelo kernel em menos de duas semanas, a partir de vários anos de trabalho voluntário em Lean. Esse é um resultado real sobre velocidade de tradução. Não é um resultado sobre descoberta matemática, e o próprio README admite a lacuna residual: "What no tool can check is that each intermediate theorem means what its name suggests."