AIREITERSe a manchete diz que “Claude resolveu o Último Teorema de Fermat”, preste atenção a uma palavra: formalizou. A Anthropic publicou um artefato em Lean que, segundo a empresa, verifica o teorema de ponta a ponta. Mas o caminho matemático usado é o já conhecido argumento de Frey–Serre–Ribet–Wiles–Taylor-Wiles — não uma prova inédita descoberta pela IA.
Antes de tudo, separe as duas afirmações
A resposta curta é sim: a Anthropic publicou um repositório contendo uma formalização do Último Teorema de Fermat (FLT) em Lean 4, com instruções para compilação e verificação. Já a ideia de que Claude resolveu o famoso problema de forma independente não é correta; o avanço matemático foi obtido por Andrew Wiles e Richard Taylor décadas atrás.
O FLT afirma que não existem soluções em inteiros positivos para a^n + b^n = c^n quando n > 2. A prova de Wiles foi publicada em 1995. O trabalho da Anthropic transforma esse caminho já estabelecido em um artefato verificável por máquina. Para conhecer o contexto histórico, consulte o anúncio do projeto de FLT da Lean Community.
Uma prova em Lean responde a uma pergunta diferente daquela feita por um artigo matemático informal. Ela pode mostrar que uma proposição codificada com precisão decorre de definições, dependências e axiomas verificados em um ambiente específico. Não pode provar que uma IA inventou a matemática subjacente nem que os nomes dos teoremas correspondem às descrições que receberam.
O que a Anthropic realmente publicou
Em seu artigo de pesquisa de 4 de setembro de 2026, a Anthropic afirma que Claude produziu a primeira formalização completa, de ponta a ponta e verificada por computador do FLT em Lean, em 11 dias. O texto menciona aproximadamente 13 milhões de linhas de Lean, 30.300 declarações de teoremas provadas e 29.500 usadas na prova final. Também foram gerados cerca de 6 bilhões de tokens.
O trabalho usou o Prove2Me, plataforma que a Anthropic descreve como responsável por manter um grafo acíclico direcionado de declarações de teoremas e coordenar vários agentes. Segundo a empresa, a formalização segue uma versão simplificada do caminho de prova estabelecido e associado a Frey, Serre, Ribet, Wiles e Taylor-Wiles.
Para verificar a afirmação, o repositório público no GitHub é mais útil do que o anúncio. O alvo padrão é o arquivo FinalCheck.lean, cuja declaração do teorema é:
theorem fermat_last_theorem (n : ℕ) (hn : 3 ≤ n) (a b c : ℕ)
(ha : 0 < a) (hb : 0 < b) (hc : 0 < c) :
a ^ n + b ^ n ≠ c ^ nO próprio repositório se identifica como um artefato de pesquisa que não é mantido e não aceita contribuições. Ele fixa o Lean 4.33.1 e o Mathlib v4.33.0, inclui o arquivo PROOF-PATH.md e oferece uma versão HTML navegável offline do grafo de teoremas e definições.
A verificação final do repositório foi projetada para falhar caso a prova dependa de um axioma adicionado, sorry, native_decide, unsafe ou outro mecanismo de escape semelhante. Isso torna o artefato auditável, sem exigir que o leitor confie apenas em uma captura de tela ou em um resumo escrito.
Como reproduzir a verificação
Uma checagem séria começa pelo ambiente fixado no repositório, não pela cópia de um arquivo .lean isolado para outro projeto. O guia de verificação da Lean Community explica o motivo: o Lean lança versões mensalmente, o Mathlib muda com frequência e a compatibilidade retroativa não é garantida.
Fixe o ambiente antes de compilar
O repositório informa que a compilação foi pensada para Linux ou macOS e exige elan, Git, Python, GNU coreutils e uma conexão de rede para que o Lake possa baixar e compilar as dependências fixadas. O projeto ocupa cerca de 67 GB em .lake, além de aproximadamente 220 GB de arquivos C gerados, que podem ser apagados depois.
O repositório também informa um consumo de cerca de 5 GB de memória por trabalho paralelo, com alguns módulos exigindo até 36 GB. Com 96 trabalhos, a compilação registrada pelo próprio projeto levou 5 horas e 32 minutos e atingiu um pico de 153 GB de memória. Esses números foram informados pelo repositório, não medidos neste artigo; use-os como um alerta de planejamento, e não como garantia de tempo de execução.
Escolha um caminho de verificação
- Apenas inspecionar: leia
FinalCheck.lean,PROOF-PATH.mdeATTRIBUTION.mdsem compilar. - Compilação completa em Lean: use a toolchain fixada e execute
lake build. - Reprodução independente: depois de uma compilação e exportação bem-sucedidas, execute os scripts do comparator e do nanoda.
A partir de um clone novo, o repositório fornece esta sequência geral:
git clone https://github.com/anthropics/fermats-last-theorem.git flt
cd flt
# Lower the number if your machine cannot supply the required memory.
LEAN_NUM_THREADS=96 lake build
# Check the result against a Mathlib-only challenge statement.
verification/comparator/run.sh
# Run after the comparator check.
verification/nanoda/run.shCada etapa tem uma função diferente:
| Etapa | Detalhe informado pelo repositório | Para que serve |
|---|---|---|
lake build | 60.475 módulos; 5 h 32 min com 96 trabalhos na execução registrada | Compila o projeto a partir do código-fonte e permite que o kernel do Lean verifique as declarações incluídas na compilação |
| Comparator | 14 h 46 min na execução registrada; pico de memória de 230 GB | Verifica se o teorema exposto e as constantes referenciadas correspondem à declaração de desafio pretendida do Mathlib |
nanoda | Cerca de 30 minutos com 16 threads após a exportação | Reproduz um ambiente exportado usando um kernel independente do Lean, escrito em Rust |
O comparator não substitui a leitura da declaração do teorema. Ele ajuda a reduzir o risco de um projeto provar uma proposição enfraquecida ou sutilmente diferente. O PROOF-PATH.md do repositório relaciona as etapas matemáticas nomeadas às declarações em Lean, enquanto as páginas HTML geradas permitem inspecionar as dependências sem executar uma aplicação web.
O repositório informa custos adicionais para as duas verificações: gravar uma exportação de 37,8 GB pode exigir cerca de 90 GB de memória, e o fluxo de trabalho do nanoda pode precisar de cerca de 40 GB durante a verificação.
O que as evidências comprovam — e o que não comprovam
| Camada de evidência | Estabelece | Não estabelece |
|---|---|---|
| Compilação do kernel do Lean | Os termos de prova enviados passam pela verificação de tipos no ambiente fixado do Lean | Que Claude descobriu a matemática ou que a explicação informal corresponde a cada nome de teorema |
FinalCheck.lean e proteção contra axiomas | O teorema final do repositório é verificado em relação à lista de axiomas informada e rejeita vários atalhos listados | Que o teorema corresponde à formulação histórica do FLT sem que a própria declaração seja inspecionada |
Saída de #print axioms | As dependências incluem os axiomas padrão do Lean propext, Classical.choice e Quot.sound, em vez de um axioma de usuário oculto, quando a verificação esperada passa | Que toda a cadeia de fornecimento de software foi validada de forma independente |
| Comparator | O resultado provado e as constantes referenciadas correspondem ao desafio baseado apenas no Mathlib usado pelo repositório | Que todas as descrições em linguagem natural do projeto são claras ou pedagogicamente adequadas |
| Reprodução com nanoda | Um ambiente exportado foi aceito por uma segunda implementação do kernel do Lean, escrita em Rust | Que a exportação, os scripts ou o sistema operacional estão livres de qualquer possível erro |
PROOF-PATH.md e atribuição | Um caminho para que humanos inspecionem a correspondência matemática e as fontes anteriores | Que nomes de teoremas gerados por máquina descrevem corretamente suas declarações sem revisão humana |
A lista “Did you prove it?” da Lean Community resume a regra principal: a compilação valida a proposição codificada, não se o nome de um teorema corresponde à afirmação informal pretendida. Neste artefato, o comparator e o uso do Mathlib reduzem esse risco, mas não eliminam a necessidade de ler a declaração do teorema e o caminho da prova.
O que o artefato mostra — e o que não mostra
O sistema produziu um artefato em Lean formalmente verificado e de escala incomum. Isso não demonstra um novo caminho para o FLT, uma nova prova elementar nem uma descoberta matemática independente feita por Claude.
A Anthropic afirma que a prova segue uma versão simplificada do caminho de Wiles. O repositório também dá crédito a trabalhos existentes: seu ATTRIBUTION.md identifica 106 arquivos com material do projeto de FLT do Imperial College London ou do flt-regular, além do Mathlib. Essa procedência é essencial para descrever com precisão em que o artefato publicado se baseia.
O projeto informa que 30.300 declarações de teoremas foram provadas durante a execução e que cerca de 29.500 foram usadas na prova final, enquanto o repositório descreve 29.511 páginas de teoremas. São declarações e dependências formais, não 29.511 resultados matemáticos recém-descobertos. Uma prova formal expande etapas implícitas, tipos, coerções, definições e dependências de bibliotecas que uma prova humana pode deixar ao conhecimento especializado do leitor.
O repositório diz que seus arquivos-fonte foram escritos para serem verificados, não para serem lidos: os nomes são gerados por máquina, rótulos como P2M identificam etapas do pipeline e a declaração, não o nome, é o que tem autoridade. Por isso, o caminho da prova e o comparator são tão importantes quanto o teorema destacado na manchete.
Os trabalhos anteriores em Lean não devem ser misturados à afirmação de 2026. Um artigo de 2023 sobre o Último Teorema de Fermat para primos regulares apresentou uma formalização completa e sem sorry do Caso I do teorema de Kummer para primos regulares, observando que o Caso II e o lema de Kummer ainda exigiam um trabalho substancial. Uma revisão de 2025 descreveu a formalização para primos regulares como uma prova completa desse caso mais específico.
| Trabalho | Escopo | Função prática |
|---|---|---|
Pesquisa do flt-regular | Resultados sobre primos regulares e infraestrutura de apoio em teoria algébrica dos números | Bloco formal anterior e material de origem |
| Projeto de FLT do Imperial | Formalização de longo prazo e reutilizável da teoria moderna dos números relacionada ao FLT | Infraestrutura de bibliotecas e colaboração |
| Repositório da Anthropic | Uma alegada formalização de ponta a ponta do teorema de FLT em Lean 4, com verificações de compilação e reprodução | Um artefato de pesquisa de grande escala, otimizado para um resultado verificado, e não para manutenção de longo prazo |
O projeto de FLT do Imperial/Lean descreve a formalização da teoria moderna dos números como um esforço mais amplo de infraestrutura, e não apenas como a tradução de um teorema. A publicação da Anthropic deve ser entendida como uma evidência complementar sobre o que agentes de IA coordenados conseguem fazer dentro de um ecossistema formal já existente — não como prova de que os objetivos do projeto anterior deixaram de ser relevantes.
O que cada público pode concluir
| Se você quer saber… | A resposta responsável é… | Próximo passo |
|---|---|---|
| Se a Anthropic publicou um artefato real | Sim; há um anúncio oficial e um repositório público com ambiente fixado | Leia o artigo de pesquisa e o repositório em conjunto |
| Se o teorema codificado é o FLT | O repositório fornece uma declaração específica, um comparator e um caminho da prova | Inspecione FinalCheck.lean, o comparator e o PROOF-PATH.md |
| Se o código compila corretamente | O repositório documenta uma compilação do zero e informa o próprio resultado | Recompile com Lean 4.33.1 e Mathlib v4.33.0 se você tiver o hardware necessário |
| Se Claude inventou uma nova prova | Não há evidências que sustentem essa descrição; o caminho usa a matemática estabelecida de Wiles/Taylor-Wiles | Descreva o trabalho como formalização assistida por IA ou engenharia de provas |
| Se o artefato é fácil de manter | Não; o repositório afirma explicitamente que não é mantido, e o código é gerado por máquina | Trate-o como um artefato de pesquisa, não como uma biblioteca pronta para integração ao Mathlib |
| Se isso prova uma autonomia matemática geral | Não; o resultado mostra desempenho em um alvo de formalização altamente especificado e com bastante infraestrutura de apoio | Separe a capacidade de verificação formal da descoberta aberta de teoremas |
Se você só precisa entender a notícia, o lançamento oficial e o repositório comprovam que o projeto existe. Se precisa fazer uma auditoria, reproduza a compilação no ambiente fixado e inspecione a declaração. Se está avaliando pesquisa em IA, considere também a orquestração, as bibliotecas existentes, a formalização anterior e o poder computacional usado.
Perguntas frequentes
Claude descobriu uma nova prova do Último Teorema de Fermat?
Não. O artefato da Anthropic formaliza um caminho de prova já estabelecido e associado a Frey, Serre, Ribet, Wiles e Taylor-Wiles. A conquista está na escala e na velocidade da produção de um artefato em Lean verificável por máquina, não em uma nova solução matemática.
Uma compilação bem-sucedida em Lean prova o teorema informal?
Ela prova que a proposição codificada decorre das dependências verificadas naquele ambiente Lean. Ainda é preciso confirmar que a proposição e suas definições correspondem ao teorema informal que você pretende afirmar.
O repositório usa sorry ou axiomas adicionais?
O repositório afirma que sua verificação final rejeita sorry, axiomas adicionados, native_decide, unsafe e vários atalhos relacionados. A lista de axiomas esperada contém os três axiomas padrão do Lean: propext, Classical.choice e Quot.sound. Reproduza a verificação em vez de confiar apenas no anúncio.
Posso reproduzir o resultado em um laptop comum?
Talvez seja possível inspecionar e compilar parcialmente o repositório, mas a verificação completa não é uma tarefa leve e comum. O repositório informa um pico de 153 GB de memória na compilação, até 230 GB no comparator e grandes exigências de armazenamento. Portanto, o hardware é uma limitação central.
Para avaliar a afirmação com precisão, comece pelo artefato fixado no GitHub, leia a declaração do teorema antes de se deixar levar pela manchete e descreva o resultado como uma grande formalização, assistida por IA, de uma matemática já conhecida.