Modelo Claude da Anthropic formaliza prova do Último Teorema de Fermat
IA da Anthropic concluiu a formalização do Último Teorema de Fermat na linguagem Lean de forma majoritariamente autônoma em apenas 11 dias.
Pontos principais
- O modelo Claude utilizou a linguagem Lean e a biblioteca Mathlib para realizar a formalização.
- O processo de verificação matemática foi concluído em 11 dias, tempo significativamente menor que o estimado por especialistas.
- A prova formalizada compreende mais de 13 milhões de linhas de código.
- O trabalho incluiu a verificação de mais de 29.000 teoremas auxiliares para validar o resultado final.
A Anthropic anunciou que seu modelo de inteligência artificial, Claude, completou a primeira prova formalizada do Último Teorema de Fermat. O processo, que envolveu a tradução do raciocínio matemático para a linguagem de programação Lean, foi executado de forma majoritariamente autônoma ao longo de 11 dias. A conquista representa um avanço significativo na aplicação de LLMs em tarefas de verificação formal, um campo onde a precisão é crítica e que tradicionalmente demanda anos de trabalho humano. Ao todo, o projeto resultou em mais de 13 milhões de linhas de código e na validação de 29.000 teoremas auxiliares, demonstrando a capacidade da IA em lidar com estruturas lógicas complexas e extensas. A utilização da biblioteca Mathlib foi fundamental para que o sistema alcançasse a verificação completa do teorema de forma eficiente.
Tópicos relacionados
Cobertura da mídia
Anthropic says Claude worked "largely autonomously" over 11 days to formalize the proof of Fermat's Last Theorem in the Lean programming language (Anthropic)
Techmeme • 4 set, 17:35
@AnthropicAI: Checking that a major mathematical proof is correct can take years. Formalization—converting the mathematical reasoning into a form computer proof assistants like Lean can verify—c…
x.com • 4 set, 15:50