Uma demonstração que um computador consegue conferir
A Anthropic anunciou em 4 de setembro que um modelo interno de pesquisa produziu a primeira demonstração do último teorema de Fermat verificável de ponta a ponta por computador. A formalização ocupa cerca de 13 milhões de linhas de Lean, o assistente de provas que os matemáticos usam para obrigar cada passo de um argumento a assumir uma forma que a máquina possa conferir. O trabalho levou onze dias, segundo a empresa.
O último teorema de Fermat afirma que nenhum trio de inteiros positivos satisfaz a^n + b^n = c^n para qualquer inteiro n maior que dois. Andrew Wiles o demonstrou em 1995 num artigo de cerca de 129 páginas, apoiado em maquinaria construída ao longo do século XX. Conferir uma demonstração dessas à mão leva anos aos especialistas. Formalizá-la deveria levar prazo comparável.
O que o modelo de facto fez
Segundo a Anthropic, tratava-se de um modelo interno de uso geral, aproximadamente comparável ao Claude Fable 5.1, e não de um motor matemático dedicado. Várias dezenas de agentes trabalharam em paralelo, gerando cerca de seis mil milhões de tokens e demonstrando 30 300 teoremas, dos quais 29 500 constam do resultado final. A intervenção humana limitou-se a orientação de alto nível.
A Anthropic diz que as primeiras tentativas falharam por completo. A execução bem-sucedida dependeu de uma plataforma interna chamada Prove2Me, que regista quais teoremas dependem de quais e permite que muitos agentes trabalhem em ramos distintos da mesma demonstração sem perder o fio. Cerca de sete por cento das linhas não rotineiras do ficheiro final vieram das tentativas falhadas.
O trabalho humano por baixo
O resultado não surgiu do nada. Segue uma versão simplificada do argumento de Wiles apresentada por Henri Darmon, Fred Diamond e Richard Taylor, e assenta na Mathlib, a biblioteca matemática comunitária que milhares de colaboradores constroem em Lean há mais de uma década, e no projeto de formalização dirigido por Kevin Buzzard no Imperial College de Londres. Buzzard, que reviu o resultado, resumiu a importância em termos de fiabilidade: os artefactos, disse, já são robustos o suficiente para se construir sobre eles.
A própria Anthropic apontou limites. A demonstração assenta apenas nos três axiomas padrão do Lean, e um comparador confirmou que o enunciado demonstrado coincide com a formulação do teorema na Mathlib — a verificação que impede um sistema de demonstrar algo subtilmente mais fraco do que afirma. Mas a empresa também reconhece que a demonstração é provavelmente muito mais longa do que precisa de ser, o que importa a quem queira reaproveitar as peças.
Porque o interessante é a formalização
A matemática arrasta há décadas um estrangulamento na verificação: as demonstrações de fronteira são tão longas que apenas um punhado de pessoas as consegue arbitrar, e alguns erros sobreviveram à publicação. A formalização elimina o problema do árbitro, ao custo de uma quantidade enorme de trabalho fastidioso. Essa troca manteve-a rara.
Se a metade fastidiosa puder ser automatizada nesta escala, a conta muda. Junta-se ainda a uma série de anúncios semelhantes: a Anthropic publicou em agosto trabalho sobre novos resultados obtidos pelo Claude em torno da função zeta de Riemann, e a OpenAI afirmou que o seu modelo Astra resolveu vários problemas de Erdős em aberto.
O que convém acompanhar é a reutilização independente. Um ficheiro Lean de 13 milhões de linhas é verificável por construção — é para isso que o Lean serve — mas o seu valor para matemáticos no ativo depende de os teoremas intermédios poderem ser incorporados na Mathlib e usados noutros contextos. A Anthropic não disse quando, nem se, publicará o artefacto completo para isso.
