A Anthropic afirmou que o Claude completou a primeira prova formalizada completa do Último Teorema de Fermat. Não se trata de uma redescoberta do teorema, mas sim da reescrita da prova existente em código lógico verificável linha por linha por um computador. A empresa afirmou que o trabalho levou 11 dias e resultou em aproximadamente 13 milhões de linhas de conteúdo.
O significado da prova formal reside em transformar argumentos matemáticos em linguagem verificável por máquina. Provas em artigos tradicionais frequentemente exigem revisão prolongada por pares; se houver uma falha em algum passo intermediário, o processo de correção pode durar meses ou até anos. O Último Teorema de Fermat foi provado pelo matemático britânico Andrew Wiles em 1995, mas transformar completamente essa prova em uma versão verificável por máquina sempre foi considerado um projeto de alta intensidade.
Concluir o objetivo do projeto de longo prazo em 11 dias
O matemático do Imperial College London, Kevin Buzzard, tem impulsionado o projeto desde 2024, com o mesmo objetivo de reescrever a prova de Wiles no assistente de prova Lean. Conforme planejado originalmente, este trabalho requer colaboração prolongada, com financiamento garantido até 2029.
A Anthropic afirmou que o Claude concluiu antecipadamente esse objetivo comparável. Após revisão por Buzzard, foi constatado que esta prova pode ser estabelecida sem depender de suposições adicionais, ou seja, validada apenas com base nos axiomas mais fundamentais da matemática.
Concluído em paralelo por múltiplos agentes
Segundo a Anthropic, a equipe do pesquisador da Universidade de Columbia, Tianyi Peng, fez múltiplos agentes Claude trabalharem em paralelo, cada um responsável por escrever definições e provar conclusões menores, depois unindo-as progressivamente em estruturas de prova maiores. A intervenção humana foi mínima, consistindo principalmente em definir prioridades阶段.
Os avanços iniciais não foram fáceis. A Anthropic relatou que alguns agentes, em determinado momento, não conseguiam compartilhar conteúdo concluído e acabavam realizando trabalho duplicado. Em seguida, a equipe utilizou uma ferramenta chamada Prove2Me para fornecer a todos os agentes uma lista unificada de tarefas e uma estrutura de arquivos, além de manter observações em linguagem natural, ajudando-os a reutilizar os resultados uns dos outros.
- Mais de 30 mil teoremas de suporte
- O consumo total atingiu bilhões de tokens
- Finalmente comprovado cerca de 13 milhões de linhas
Focus on verifiability rather than new theorems
O foco deste avanço não está em descobrir novos teoremas matemáticos, mas em transformar provas já significativas em versões verificáveis passo a passo por computador. Com o aumento de artigos matemáticos e conteúdo gerado por IA, o custo de verificação manual de provas também está aumentando, tornando as ferramentas de formalização cada vez mais relevantes.
A Anthropic também afirmou que o tamanho desta prova é mais de cinco vezes maior do que a biblioteca compartilhada comumente usada na comunidade matemática, a Mathlib. O arquivo completo foi carregado no GitHub, permitindo que pesquisadores continuem revisando linha por linha sua estrutura e correção.