Formalizando o Último Teorema de Fermat

Artigo original ↗ Discussão no Hacker News ↗

Um sistema de IA produziu uma formalização completa em Lean do Último Teorema de Fermat em 11 dias, gerando 13 milhões de linhas de código de prova verificado por máquina para um dos resultados mais famosos da matemática moderna. Os comentadores veem isso como um marco para a demonstração automática de teoremas e métodos formais, mas levantam preocupações sobre a confiança na verificação (possíveis bugs em assistentes de prova), a legibilidade das provas e se formalizações gigantes geradas por IA são realmente reutilizáveis ou significativas para humanos. O thread também explora implicações mais amplas: o custo e a eficiência do raciocínio em larga escala por IA, o impacto nas carreiras matemáticas e no financiamento de pesquisa, e se futuros sistemas poderão passar de formalizar provas conhecidas a descobrir provas fundamentalmente novas.

Natureza do resultado

  • O thread enfatiza que isto não é uma nova prova matemática do Último Teorema de Fermat (FLT), mas sim uma formalização em Lean de uma prova existente no estilo de Wiles/Taylor.
  • Vários comentários observam que a comunidade matemática já considerava o FLT essencialmente resolvido; a novidade está na escala e na velocidade da autoformalização.
  • A formalização segue uma exposição dos anos 1990, não as abordagens mais modernas e enxutas, e trata dos primos ≥17; outras formalizações anteriores cobrem os casos restantes.

Escala, custo e ferramentas

  • Claude produziu cerca de 13M de linhas de Lean e ~29,5k lemas em ~11 dias, usando ~6B tokens de saída e grande poder de computação (centenas de GB de RAM, muitos núcleos).
  • Estimativas de custo com preços públicos de API ficam na casa de centenas de milhares de dólares, mas há debate sobre se a inferência interna é muito mais barata e sobre como amortizar o custo de treinamento.
  • Uma plataforma colaborativa de Lean (prove2.me) e uma orquestração personalizada (“swarm of agents”) foram essenciais; alguns veem isso como evidência de que ferramentas estruturadas são cruciais para trabalhos sérios.

Confiança, correção e o kernel do Lean

  • Muitos perguntam: como confiar em 13M de linhas? A resposta: o verificador de tipos do Lean valida cada passo; os humanos precisam principalmente confiar em:
    • a declaração formal do FLT,
    • o kernel pequeno e os axiomas,
    • e um verificador secundário (“comparator”) que revalida o teorema final.
  • Outros alertam que o Lean teve bugs recentes de correção, incluindo uma “refutação” do Collatz encontrada por IA que explorava um bug do kernel; múltiplos verificadores independentes reduzem, mas não eliminam o risco.
  • Alguns querem a tradução para outros sistemas (por exemplo, HOL/Metamath) para garantia adicional.

Valor para a matemática e reutilização

  • Defensores: grandes esforços de prova normalmente geram muitas abstrações reutilizáveis; a autoformalização pode detectar erros na literatura e reduzir o trabalho dos revisores.
  • Céticos: 13M de linhas podem ser “AI slop” com abstrações ruins, difíceis de integrar em bibliotecas padrão; talvez não avancem a compreensão humana.
  • Um projeto humano em andamento de formalização do FLT tinha objetivos diferentes: contribuir com componentes de mathlib limpos e gerais e um “documento dinâmico” explorável por humanos.

Impacto sobre matemáticos e carreiras

  • Emoções mistas: admiração pela capacidade, preocupação com pesquisadores no início da carreira sendo “passados para trás” por LLMs.
  • Alguns argumentam que formalizar é distinto de descobrir provas, então ainda existe um grande papel para a criatividade e a exposição humanas.

Implicações mais amplas da IA e ética

  • Otimistas veem isto como evidência de que a IA pode atacar grandes parcelas da matemática e, por analogia, problemas científicos (por exemplo, medicina, física).
  • Pessimistas se preocupam com concentração de poder, orçamentos de computação opacos, hype para IPOs e acesso público limitado aos modelos mais fortes.
  • Aparece debate filosófico sobre significado humano, “brincar de Deus” (por exemplo, curar o envelhecimento) e se o progresso da IA melhora ou prejudica o bem-estar humano.

Direções futuras

  • Próximos alvos sugeridos: classificação dos grupos simples finitos, Hipótese de Riemann, P vs NP.
  • Vários querem que futuras passagens de IA simplifiquem e refatorizem radicalmente a formalização do FLT, ou mostrem que ela é quase mínima em algum sentido formal.