Claude formaliza a demonstração do teorema de Fermat em Lean

A Anthropic anunciou a 4 de setembro de 2026 que a sua IA Claude produziu a primeira demonstração do último teorema de Fermat totalmente verificável por computador, do início ao fim. O teorema afirma que não existem inteiros positivos a, b, c que satisfaçam a^n + b^n = c^n para nenhum inteiro n superior a 2. Mais de trinta anos depois de o matemático Andrew Wiles ter publicado a sua demonstração de 129 páginas em 1995, ninguém tinha verificado mecanicamente toda a sua lógica desde o início. Claude trabalhou de forma largamente autónoma durante 11 dias e produziu cerca de 13 milhões de linhas de código em Lean, um assistente de provas informático.

O projeto foi liderado por Tianyi Peng, investigador da Anthropic especializado em formalização matemática com IA. Ao longo do processo, Claude demonstrou, de forma verificável por computador, cerca de 30.300 teoremas intermédios, dos quais aproximadamente 29.500 foram efetivamente usados na demonstração final. O código produzido é mais de cinco vezes maior do que o Mathlib, a principal biblioteca matemática comunitária do Lean. Dezenas de agentes Claude trabalharam em paralelo a definir conceitos e a demonstrar teoremas intermédios antes de avançarem para afirmações mais difíceis. As primeiras tentativas falharam: os agentes perdiam a noção do estado geral do projeto e deixavam de reaproveitar eficazmente os resultados uns dos outros. Cerca de 7% das linhas não repetitivas da demonstração final resultam dessas tentativas falhadas.

O que é uma demonstração formal verificada por computador

Um artigo de matemática escrito para leitores humanos costuma omitir passos considerados "óbvios". Um assistente de provas como o Lean não pode fazê-lo: cada passo, por mais trivial que seja, tem de ser escrito por extenso. Reescrever uma demonstração existente nesse formato chama-se "formalização". Como um único elo lógico quebrado pode invalidar tudo o que se segue, uma demonstração formalizada só obtém uma garantia de correção independente da revisão humana depois de passar pela verificação mecânica do Lean. A de Claude depende apenas dos três axiomas padrão do Lean, sem qualquer utilização de "sorry" — o marcador que permite deixar um passo temporariamente por demonstrar. Uma ferramenta de comparação confirmou que o enunciado demonstrado corresponde ao do último teorema de Fermat tal como consta no Mathlib, e um núcleo Lean independente escrito em Rust, chamado "nanoda", verificou mais de um milhão de declarações sem qualquer erro.

Por que o teorema de Fermat é um caso tão emblemático

O teorema deve o nome a uma nota que o matemático francês Pierre de Fermat rabiscou por volta de 1637 na margem de um exemplar da Aritmética de Diofanto, onde afirmava ter encontrado "uma demonstração verdadeiramente maravilhosa" que a margem era demasiado estreita para conter. Durante mais de 350 anos, gerações de matemáticos procuraram essa demonstração sem sucesso. Em 1908, foi oferecido um prémio equivalente hoje a um a dois milhões de dólares a quem a encontrasse; só no primeiro ano surgiram 621 tentativas erradas. Em junho de 1993, Andrew Wiles anunciou a sua demonstração numa série de conferências de três dias, mas cerca de dois meses depois, durante a revisão, um avaliador detetou uma falha crítica. Levou quase um ano, com o seu antigo aluno Richard Taylor, a corrigi-la antes de publicar a versão definitiva em maio de 1995 — 129 páginas, cuja verificação levou meses de trabalho à comunidade matemática. Um pormenor relevante para um leitor internacional: a conjetura de Taniyama-Shimura, na qual assenta a demonstração de Wiles, foi formulada nos anos 1950 pelos matemáticos japoneses Yutaka Taniyama e Goro Shimura. O que Claude formalizou é uma versão simplificada da demonstração de Wiles, devida a Darmon, Diamond e Taylor.

Esta extraordinária conquista de autoformalização, que segundo os investigadores da Anthropic demorou apenas 11 dias, demonstra o teorema de Fermat sem quaisquer hipóteses além dos axiomas da matemática. Ao longo do processo, vemos a autoformalização de álgebra, análise harmónica, geometria e teoria dos números, e ficamos a saber que os artefactos de autoformalização produzidos por IA já são suficientemente robustos para se construir sobre eles: a demonstração está organizada em várias camadas.

• Duração do trabalho: 11 dias, largamente autónomo
• Código Lean produzido: cerca de 13 milhões de linhas, mais de 5 vezes o Mathlib
• Teoremas demonstrados: cerca de 30.300, dos quais 29.500 usados na demonstração final
• Tokens de saída consumidos: cerca de 6 mil milhões, com um modelo de investigação comparável ao Claude Fable 5.1
• Axiomas utilizados: apenas os 3 axiomas padrão do Lean, zero utilizações de "sorry"

O que Claude realmente fez — e o que não fez

Convém sublinhar que Claude não "descobriu" sozinho a demonstração original de Wiles. O raciocínio matemático foi estabelecido por Wiles e pelos seus colaboradores em 1995; o trabalho de Claude consistiu em reescrever uma versão simplificada desse raciocínio na forma simbólica rigorosa que o Lean consegue verificar, submetendo-a depois a uma verificação mecânica — isso é formalização, não descoberta. É diferente dos trabalhos recentes de IA sobre a hipótese de Riemann, orientados para produzir matemática genuinamente nova. A própria Anthropic é explícita: a novidade aqui está na verificação, não na descoberta. O trabalho apoiou-se no Prove2Me, uma plataforma colaborativa de formalização matemática criada por Tianyi Peng, que gere as dependências entre teoremas através de um grafo acíclico dirigido, para que vários agentes Claude saibam qual o teorema a atacar a seguir. A intervenção humana limitou-se a instruções de alto nível de Peng, como "dar prioridade ao jacobiano enquanto esquema".

À medida que a IA produz mais demonstrações matemáticas, aumenta o peso de as rever manualmente. A Anthropic espera que produzir uma demonstração formalizada e verificável por computador, a par de um artigo pensado para leitores humanos, se torne prática comum. Kevin Buzzard, que lidera desde 2024 um projeto comunitário plurianual para formalizar o teorema de Fermat em Lean no Imperial College London — cujo plano de trabalho inicial já soma 86 páginas —, classificou esta conquista como um grande passo rumo à autoformalização da literatura matemática moderna: detetar erros no corpo de conhecimento existente, aliviar a carga dos revisores, e permitir verificar rigorosamente matemática gerada por IA.

Para uma empresa portuguesa de tecnologia, a lição vai além do feito matemático em si. Os mesmos assistentes de prova que verificaram este teorema já são usados para verificar protocolos criptográficos, compiladores e código crítico em setores como a aeronáutica ou o desenho de semicondutores — áreas onde centros de investigação nacionais, como o INESC-ID ou a Universidade do Minho, já trabalham em métodos formais. Um agente de IA capaz de produzir milhões de linhas de prova verificada por máquina em dias, e não em anos, é um sinal concreto de que a verificação formal, durante muito tempo considerada demasiado lenta e especializada para escalar, pode tornar-se bastante mais acessível a equipas de engenharia fora da matemática pura — desde que, como a própria Anthropic sublinha, esta capacidade de verificação nunca seja confundida com uma capacidade de descobrir matemática nova de forma autónoma.