Último Teorema de Fermat: o problema que levou 358 anos

O Último Teorema de Fermat diz que não existem números inteiros positivos a, b e c que satisfaçam a equação aⁿ + bⁿ = cⁿ quando n é maior que 2. Ele foi anotado por Pierre de Fermat por volta de 1637 e só foi provado em 1995, pelo matemático britânico Andrew Wiles, cerca de 358 anos depois. O problema voltou ao noticiário porque a Anthropic anunciou que seu modelo de inteligência artificial, o Claude, completou a primeira prova formalizada do teorema, conferindo cada passo em uma linguagem que o computador consegue verificar.

O que diz o teorema

Muita gente conhece a equação de Pitágoras: em um triângulo retângulo, a² + b² = c². Ela tem infinitas soluções com números inteiros, como 3, 4 e 5 (9 + 16 = 25).

Fermat se perguntou o que acontece quando o expoente aumenta. Existem inteiros positivos que satisfaçam a³ + b³ = c³? Ou a⁴ + b⁴ = c⁴? A resposta que ele propôs foi não: para qualquer expoente maior que 2, nenhuma combinação de inteiros positivos funciona.

O enunciado é tão simples que pode ser entendido por um estudante do ensino médio. Provar que ele vale para todos os expoentes, porém, desafiou alguns dos maiores matemáticos da história.

A anotação na margem

Pierre de Fermat era um jurista francês que fazia matemática nas horas vagas e se tornou um dos nomes mais importantes da teoria dos números. Ele costumava escrever observações nas margens de seu exemplar da Aritmética, obra do matemático grego Diofanto.

Em uma dessas notas, ao lado de um problema sobre quadrados, Fermat escreveu que havia encontrado uma demonstração realmente maravilhosa para a afirmação, mas que a margem era estreita demais para contê-la. A anotação só se tornou pública depois de sua morte, quando o filho publicou uma edição do livro com os comentários do pai.

Hoje, a maioria dos matemáticos acredita que Fermat não tinha uma prova completa. As ferramentas usadas na solução final só seriam criadas séculos depois.

Três séculos de tentativas

O próprio Fermat deixou uma prova para o caso do expoente 4. No século 18, Leonhard Euler apresentou uma demonstração para o expoente 3. Ao longo do século 19, outros matemáticos, como Sophie Germain e Ernst Kummer, avançaram em grandes famílias de casos, mas ninguém conseguia uma prova geral.

O teorema ganhou fama justamente por isso: era fácil de enunciar e parecia impossível de provar. Ao tentar resolvê-lo, matemáticos acabaram criando áreas inteiras de estudo, que ficaram mais valiosas do que o próprio problema.

A prova de Andrew Wiles

A virada veio por um caminho inesperado. Nos anos 1980, ficou demonstrado que o teorema de Fermat seria verdadeiro se outra afirmação, ligada a objetos chamados curvas elípticas e formas modulares, também fosse. Essa ligação deu um alvo concreto para quem quisesse resolver o problema.

Andrew Wiles, que se encantou com o teorema ainda criança, trabalhou nele por anos, praticamente em segredo. Em 1993, anunciou a prova em uma série de palestras na Universidade de Cambridge. Durante a revisão, porém, foi encontrada uma falha em um dos argumentos. Com a ajuda de seu ex-aluno Richard Taylor, Wiles conseguiu corrigi-la, e a demonstração completa foi publicada em 1995. O texto tem mais de cem páginas e usa matemática muito avançada.

Por que uma IA conferir a prova importa

Uma prova matemática no papel é verificada por especialistas que leem cada argumento. Em demonstrações longas e complexas, como a de Wiles, esse processo leva meses e depende de poucas pessoas capazes de acompanhar todos os detalhes.

A formalização é diferente. O raciocínio é traduzido para uma linguagem de programação especial, chamada de assistente de provas, em que o computador checa cada passo de forma mecânica. Nada pode ficar implícito: tudo o que um matemático chamaria de óbvio precisa ser justificado.

O que a Anthropic anunciou

Segundo a empresa, o Claude usou a linguagem Lean e a biblioteca Mathlib, um grande acervo de matemática já formalizada mantido pela comunidade. O processo foi executado de forma majoritariamente autônoma ao longo de 11 dias, tempo bem menor do que o estimado por especialistas. O resultado tem mais de 13 milhões de linhas de código e inclui a verificação de mais de 29 mil teoremas auxiliares, que são resultados intermediários necessários para chegar à conclusão final.

O que isso muda

A verificação formal é um campo em que a precisão é crítica e que tradicionalmente exige anos de trabalho humano. Se modelos de IA conseguem fazer boa parte desse trabalho, matemáticos podem conferir resultados longos com mais rapidez e confiança, e a técnica pode ajudar também em áreas em que erros custam caro, como a verificação de softwares e sistemas de segurança.

Perguntas frequentes

O que diz o Último Teorema de Fermat?

Que não existem números inteiros positivos a, b e c tais que aⁿ + bⁿ = cⁿ quando n é maior que 2. Para n igual a 2, a equação de Pitágoras, há infinitas soluções.

Quem provou o Último Teorema de Fermat?

O matemático britânico Andrew Wiles, com uma parte final feita em colaboração com Richard Taylor. A prova foi anunciada em 1993, corrigida e publicada em 1995.

Por que se diz que o problema levou 358 anos?

Porque Fermat anotou o teorema por volta de 1637, e a prova completa só foi publicada em 1995. Nesse intervalo, muitos matemáticos provaram casos específicos, mas não o resultado geral.

O que significa a IA ter formalizado a prova?

Significa que o raciocínio foi traduzido para a linguagem Lean, em que o computador verifica cada passo. O Claude fez isso em 11 dias, gerando mais de 13 milhões de linhas e verificando mais de 29 mil teoremas auxiliares.