Claude Formaliza o Último Teorema de Fermat em Lean

A Anthropic concluiu recentemente uma tarefa de pesquisa massiva. Um modelo interno trabalhou por 11 dias para formalizar o Último Teorema de Fermat usando a linguagem de prova Lean 4.

Esta não é uma nova descoberta matemática. Andrew Wiles provou este teorema em 1995. O que a Anthropic fez foi traduzir essa prova existente em código. Isso permite que um computador verifique cada passo lógico com total certeza.

A escala deste projeto é massiva: • O modelo produziu 13 milhões de linhas de código Lean. • Ele provou 30.300 teoremas intermediários. • Ele utilizou quase 6 bilhões de tokens de saída.

O modelo trabalhou majoritariamente por conta própria. Os humanos apenas deram orientações ocasionais de alto nível. O processo terminou no meio da noite, enquanto ninguém estava observando. O sistema registrou o sucesso automaticamente.

Duas coisas importantes a notar:

  1. Este modelo é uma ferramenta de pesquisa interna. Você ainda não pode acessá-lo via API. Ele não é o mesmo que os modelos Claude que você usa hoje.
  2. O real valor para os desenvolvedores reside na camada de coordenação chamada Prove2Me.

O Prove2Me é uma ferramenta de código aberto. Ele utiliza um grafo de dependência para gerenciar tarefas. Em vez de uma simples lista de verificação, ele cria um mapa de como as provas se conectam umas às outras.

Esta estrutura resolve dois grandes problemas para fluxos de trabalho de agentes:

  • Impede que múltiplos agentes realizem o mesmo trabalho.
  • Fornece aos agentes uma memória compartilhada para que não esqueçam o objetivo principal.

A maioria dos fluxos de trabalho de agentes falha porque perde o contexto ao longo do tempo. O uso de um grafo externo e compartilhado, em vez de uma longa janela de chat, mantém a tarefa no caminho certo.

Você deve estudar a arquitetura do Prove2Me se construir fluxos de trabalho de agentes. Mesmo que você não utilize os modelos de pesquisa da Anthropic, a maneira como eles coordenam as tarefas é um modelo para trabalhos de longo horizonte.

Fonte: https://dev.to/raxxostudios/claude-just-formalized-fermats-last-theorem-in-lean-3p36

Comunidade de aprendizado opcional: https://t.me/GyaanSetuAi