Como o Claude Code formalizou o Último Teorema de Fermat

Em 1637, o matemático Pierre de Fermat fez uma afirmação relativamente simples. Considere a equação xⁿ + yⁿ = zⁿ, em que as letras x, y, z e n são números positivos e inteiros (Ou seja, os números que mais usamos no dia a dia, como 1, 2 e 3. Nada de negativos ou vírgulas). Fermat escreveu que não haveria nenhuma solução válida para essa equação caso n fosse maior que 2. 

Em outras palavras: não há nenhuma combinação de números que você possa colocar no lugar de x, y e z que resulte em uma afirmação verdadeira. Segundo Fermat, a soma de xⁿ com yⁿ jamais resultaria em zⁿ.

Por que n precisa ser maior que 2? Ora, pense na equação x² + y² = z². Esse é o Teorema de Pitágoras: a soma dos quadrados dos catetos é igual ao quadrado da hipotenusa. A equação 3² + 4² = 5² , por exemplo, é verdadeira. Isso já prova que a negação de Fermat não se aplica quando n é 2.

Mas n não poderia ser 3? 4? 5? Fermat dizia que não. Mas ele jamais provou isso. O matemático disse que tinha a prova em mente, mas nunca a anotou no papel. Esse é conhecido como o Último Teorema de Fermat.

Demorou 357 anos até que alguém demonstrasse que Fermat, de fato, estava certo. Em 1994, o matemático Andrew Wiles completou a prova do teorema, o que foi considerado um marco científico do século 20. Por essa demonstração, Wiles recebeu o prêmio Abel (o “Nobel” da matemática) em 2016.

Agora, um protótipo do modelo de inteligência artificial Claude transformou essa demonstração em um código verificável de 13 milhões de linhas. O anúncio foi feito pela Anthropic, empresa responsável pelo Claude, em 4 de setembro. A IA demorou apenas 11 dias para completar o projeto. Estima-se que os humanos levariam 10 anos para fazer o mesmo.

O Claude não solucionou o problema, e sim formalizou sua prova. Ele transformou uma demonstração feita em linguagem natural (ou seja, em palavras) em uma em uma prova formal que pode ser verificada computacionalmente. Em outras palavras, ele “traduziu” a prova da linguagem humana para a linguagem lógica das máquinas. A tradução foi feita usando uma  linguagem de programação de código aberto chamada Lean.

A formalização do Teorema de Fermat se soma ao rol de avanços que as IAs têm produzido na matemática – seja checando o trabalho de pesquisadores humanos ou produzindo raciocínios inéditos. “Dois anos atrás, isso era fantasia” disse Kevin Buzzard, matemático do Imperial College de Londres, em entrevista à Nature. O pesquisador tem se dedicado à formalização do Teorema de Fermat no Lean desde 2024.

Formalizar uma demonstração matemática no Lean requer que ele “conheça” noções, argumentos e provas anteriores. Na matemática, todo o conhecimento se constrói com base em afirmações que já foram provadas e confirmadas. Para dar conta de provas cada vez mais complexas, matemáticos têm construído uma biblioteca de formalizações no Lean chamada Mathlib. Todas as formalizações incluídas passam pela curadoria de especialistas humanos.

Até pouco tempo, essa era a única forma de verificar se uma demonstração matemática estaria correta: ao longo de anos, milhares de especialistas revisam os argumentos para garantir que eles seguem um encadeamento lógico. 

Acontece que nem sempre as demonstrações são simples de verificar. Muitas são publicadas em periódicos de baixa visibilidade, que são lidos por poucas pessoas. Algumas demonstrações, então, ficam em um limbo em que sua validade não é confirmada. Consequentemente, isso trava o avanço de algumas áreas da matemática que dependem dessas demonstrações.

Muitos matemáticos esperam que a formalização feita por IA em conjunto com o Mathlib e a checagem humana possam facilitar o trabalho dos checadores de periódicos científicos e promover avanços em diferentes áreas da matemática.