Alegação de que IA formalizou Último Teorema de Fermat enfrenta questionamentos
Revisão independente e atribuição clara são necessárias para separar saída do modelo de anos de trabalho humano em bibliotecas compartilhadas
A Anthropic publicou um repositório no GitHub afirmando que seu modelo Claude gerou uma formalização completa do Último Teorema de Fermat em Lean 4, com cerca de 29.511 teoremas e 1.450 definições.
Comunidade do sistema de prova Lean e o projeto público do Imperial College liderado por Kevin Buzzard dizem que a formalização do teorema é um esforço contínuo e conduzido pela comunidade, e alertam que a atribuição a Claude exagera o papel da IA.
Um artigo de 2025 no arXiv por Best e colegas já havia formalizado o caso de primos regulares do teorema em Lean, indicando que partes do resultado já estavam formalizadas antes da divulgação da Anthropic.
Especialistas observam que o resultado alegado se apoia em ampla estruturação humana e em bibliotecas compartilhadas como a Mathlib, e por isso exigem verificação ao nível do kernel e um registro claro das contribuições humanas versus as do modelo.
O episódio põe à prova como ferramentas de IA podem acelerar trabalhos de prova formal e destaca a necessidade de padrões para checagem independente, autoria e integração de saídas de IA em fluxos de trabalho que exigem alta garantia.