Um modelo da Anthropic produziu a primeira prova completa do Último Teorema de Fermat verificada por computador, escrita na linguagem Lean. O trabalho levou 11 dias e foi divulgado no início de setembro, com repercussão na revista Nature.
O que exatamente foi feito
O Último Teorema de Fermat foi demonstrado por Andrew Wiles em 1995, e ninguém duvida do resultado. O problema é outro: a prova é longa, densa e depende de décadas de matemática acumulada. Conferir linha a linha se um argumento desse porte está correto pode consumir anos de trabalho humano.
Formalizar é converter esse raciocínio para uma linguagem que um assistente de provas — no caso, o Lean — consiga verificar mecanicamente. Foi isso que o modelo da Anthropic fez, seguindo uma versão simplificada da demonstração de Wiles e apoiando-se no projeto de formalização conduzido por Kevin Buzzard, do Imperial College London.
Os números do esforço
| Item | Resultado |
|---|---|
| Tempo total | 11 dias |
| Teoremas provados | 30.300 (29.500 usados na prova final) |
| Linhas de código Lean | cerca de 13 milhões |
| Tokens de saída consumidos | aproximadamente 6 bilhões |
O trabalho foi liderado pelo pesquisador Tianyi Peng e usou a plataforma Prove2Me, desenvolvida por ele e por colaboradores da Universidade Columbia. A peça central é um grafo acíclico dirigido de enunciados: em vez de pedir ao modelo que carregue a prova inteira na memória, o sistema quebra o problema em nós independentes que vários agentes atacam em paralelo. Tentativas anteriores, sem essa infraestrutura, falharam.
O que isso não significa
Vale separar as coisas. A IA não descobriu matemática nova, nem resolveu um problema em aberto: ela traduziu e verificou uma prova que já existia. A própria Anthropic reconhece que o resultado é provavelmente muito mais longo do que precisaria ser, e cerca de 7% das linhas não triviais vieram de tentativas que não deram certo.
Ainda assim, o marco é relevante por um motivo prático: verificação formal sempre foi o gargalo da matemática assistida por computador, porque exige trabalho humano especializado e caríssimo. Se essa etapa passa a ser barata, muda o custo de confiar em demonstrações complexas — em matemática e, mais adiante, na verificação de software crítico.