Segundo a Anthropic: Último Teorema de Fermat formalizado em Lean

O momento decisivo deste projeto sobre Fermat é pouco espetacular: no Lean, uma demonstração é compilada — ou não é. No repositório do Anthropic no GitHub encontra-se agora, segundo a empresa, uma versão totalmente verificada por computador do Último Teorema de Fermat. O matemático Kevin Buzzard já compilou pessoalmente o código e executou o comparador correspondente.

Do ponto de vista matemático, o teorema não é novo. Andrew Wiles provou, em 1995, ao longo de 129 páginas, que a equação xⁿ + yⁿ = zⁿ não tem soluções inteiras para expoentes inteiros n > 2. A novidade está na formalização: a demonstração é traduzida para código de modo a que um computador possa controlar cada passo, em vez de depender de etapas intermédias omitidas por serem evidentes para os seres humanos.

O Lean é simultaneamente uma linguagem de programação e um sistema de verificação. As afirmações matemáticas e as respetivas demonstrações são verificadas com base num conjunto fixo de regras lógicas; se existir sequer uma lacuna, a demonstração não é compilada. A confiança tem de ser depositada sobretudo no pequeno núcleo do Lean e nos seus axiomas. A biblioteca disponível Mathlib limita, contudo, o campo de aplicação à parte da matemática que já foi formalizada.

Segundo a Anthropic, dezenas de agentes Claude trabalharam durante onze dias numa versão simplificada da demonstração de Wiles, baseada no trabalho de Darmon, Diamond e Taylor. O resultado foram 13 milhões de linhas de código Lean e cerca de 29 500 teoremas intermédios. Segundo a empresa, as primeiras equipas falharam na gestão global do projeto; o trabalho só avançou com o Prove2Me, uma plataforma desenvolvida pelo grupo de Tianyi Peng na Columbia University, que gere os passos seguintes da demonstração num grafo acíclico dirigido. Segundo a Anthropic, o esforço ascendeu a cerca de seis mil milhões de tokens de saída; a partir desse valor, é possível calcular custos entre 100 000 e 300 000 dólares americanos.

Na prática, isto já altera algo na formalização da literatura matemática: terceiros podem compilar o código disponibilizado e verificar a cadeia lógica. Isto cria um controlo tecnicamente reprodutível, mas não substitui uma avaliação independente, que continua, até agora, em grande medida por realizar. Buzzard considera a formalização um grande passo rumo à formalização automática da matemática moderna; ao mesmo tempo, segue a literatura inicial e não apresenta nenhuma nova afirmação matemática sobre o Último Teorema de Fermat.