Em 1637, o matemático Pierre de Fermat propôs uma afirmação sobre a equação $x^n + y^n = z^n$, onde $x$, $y$, $z$ e $n$ são números inteiros positivos. Fermat alegou que não existiria solução válida para esta equação se o expoente $n$ fosse superior a 2.
Isso significa que não há combinação de valores para $x$, $y$ e $z$ que torne a afirmação verdadeira; segundo Fermat, a soma de $x^n$ com $y^n$ nunca resultaria em $z^n$. A necessidade de $n$ ser maior que 2 pode ser contrastada com o Teorema de Pitágoras ($x^2 + y^2 = z^2$), que é verdadeiro, como exemplificado por $3^2 + 4^2 = 5^2$, provando que a negação de Fermat não se aplica quando $n=2$.
Fermat postulou que a impossibilidade de soluções persistia para $n=3$, $n=4$ e outros valores maiores, mas ele nunca registrou a prova que tinha em mente. Este conceito é conhecido como o Último Teorema de Fermat. Demoraram 357 anos para que alguém comprovasse a correção de Fermat, sendo que Andrew Wiles concluiu a prova em 1994, um evento considerado um marco científico do século XX. Por essa conquista, Wiles recebeu o Prêmio Abel em 2016.
Recentemente, um protótipo do modelo de inteligência artificial Claude transformou essa demonstração em um código verificável composto por 13 milhões de linhas. A Anthropic, desenvolvedora do Claude, divulgou este anúncio em 4 de setembro. A IA levou apenas 11 dias para concluir o projeto, enquanto estima-se que humanos levariam cerca de 10 anos para realizar o mesmo trabalho.
É importante notar que o Claude não resolveu o problema, mas sim formalizou sua prova. Ele converteu uma demonstração originalmente escrita em linguagem natural (palavras) em uma prova formal passível de verificação computacional, essencialmente traduzindo o argumento humano para a linguagem lógica das máquinas, utilizando a linguagem de programação de código aberto Lean.
Esta formalização contribui para o crescente corpo de avanços das IAs na matemática, seja auxiliando pesquisadores humanos ou gerando novos raciocínios. Kevin Buzzard, matemático do Imperial College de Londres, comentou em entrevista à Nature que, há dois anos, tal capacidade ainda era considerada ficção. O pesquisador Buzzard tem trabalhado na formalização do Teorema de Fermat no Lean desde 2024.
Para formalizar uma demonstração matemática no Lean, é necessário que o sistema conheça conceitos, argumentos e provas prévias, pois o conhecimento matemático é construído sobre afirmações já validadas. Para lidar com provas cada vez mais complexas, os matemáticos desenvolveram a Mathlib, uma biblioteca de formalizações no Lean, cujas inclusões são submetidas à curadoria de especialistas humanos.
Anteriormente, a revisão de demonstrações matemáticas dependia exclusivamente de especialistas humanos dedicando anos para verificar o encadeamento lógico dos argumentos. Contudo, muitas provas são publicadas em periódicos de menor visibilidade, limitando seu alcance e deixando sua validade incerta, o que obstrui o progresso em certas áreas da matemática que dependem delas. Muitos matemáticos esperam que a combinação da formalização por IA com a Mathlib e a checagem humana possa otimizar o trabalho dos revisores de periódicos científicos e impulsionar o avanço matemático.