A demonstração do Último Teorema de Fermat foi convertida por um protótipo do Claude em um código que pode ser verificado por computadores. O projeto, anunciado pela Anthropic em 4 de setembro, levou 11 dias e resultou em 13 milhões de linhas. A empresa estima que humanos levariam 10 anos para realizar o mesmo trabalho.
A tarefa não consistiu em resolver o problema matemático. O teorema já havia sido demonstrado pelo matemático Andrew Wiles em 1994, 357 anos depois de Pierre de Fermat fazer a afirmação original. O que a inteligência artificial fez foi transformar a demonstração, escrita em linguagem natural, em uma prova formal usando Lean, uma linguagem de programação de código aberto.
O que Fermat afirmou
Em 1637, Fermat declarou que a equação xⁿ + yⁿ = zⁿ não teria solução quando n fosse maior que 2, considerando x, y, z e n números positivos e inteiros. A afirmação não vale para n igual a 2: a equação 3² + 4² = 5² é uma aplicação do Teorema de Pitágoras.
Fermat disse ter uma prova, mas não a registrou. A confirmação veio apenas com o trabalho de Wiles, concluído em 1994. Pela demonstração, o matemático recebeu o prêmio Abel em 2016.
A verificação formal
Para formalizar uma demonstração no Lean, é necessário incorporar noções, argumentos e resultados já provados. Esse acervo é reunido na Mathlib, uma biblioteca de formalizações que passa pela curadoria de especialistas humanos.
O processo pode ajudar a conferir demonstrações matemáticas complexas. Tradicionalmente, milhares de especialistas revisam os argumentos ao longo de anos. Trabalhos publicados em periódicos de baixa visibilidade, porém, podem ser lidos por poucas pessoas e permanecer sem confirmação de validade.
Kevin Buzzard, matemático do Imperial College de Londres que trabalha na formalização do teorema no Lean desde 2024, afirmou: “Dois anos atrás, isso era fantasia”. A expectativa de matemáticos é que a combinação entre inteligência artificial, Mathlib e checagem humana facilite a revisão por periódicos científicos e contribua para avanços em diferentes áreas da matemática.
