Estamos compartilhando a primeira prova completa verificada por computador do Último Teorema de Fermat. Claude trabalhou em grande parte de forma autônoma durante 11 dias para escrever a prova na linguagem de programação Lean. Abaixo, descrevemos como a formalização foi feita e compartilhamos algumas reflexões sobre o que esse trabalho pode significar para a matemática de pesquisa.

Por volta de 1637, Pierre de Fermat anotou uma afirmação na margem de sua cópia da Arithmetica de Diofanto que se tornaria uma das conjecturas matemáticas mais famosas de todos os tempos: não há inteiros positivos a, b, c que satisfaçam aⁿ + bⁿ = cⁿ para qualquer n > 2. O Último Teorema de Fermat (FLT), como a conjectura ficou conhecida, mostrou-se incrivelmente difícil de provar. A primeira prova, de Sir Andrew Wiles em 1995, tinha 129 páginas e exigiu meses de trabalho meticuloso para verificar.

Uma década depois, o cientista da computação holandês Jan Bergstra propôs “formalizar” a prova de Wiles: converter o raciocínio matemático em uma forma que os computadores possam verificar automaticamente. Desde então, matemáticos vêm desenvolvendo os métodos necessários para codificar uma prova tão complexa, incluindo um esforço comunitário de vários anos iniciado em 2024 por Kevin Buzzard no Imperial College London para completar a formalização usando o assistente de provas Lean.

Recentemente, Tianyi Peng, pesquisador da Anthropic cujo grupo na Universidade de Columbia constrói ferramentas para formalização por IA, decidiu testar se Claude poderia progredir na formalização do FLT. O resultado foi além do que ele esperava. Em 11 dias, trabalhando em grande parte de forma autônoma, Claude produziu a primeira prova de FLT de ponta a ponta, verificada por computador. Ao longo do caminho, escreveu 13 milhões de linhas de Lean e provou 29.500 teoremas intermediários.