Lean valida prova de Fermat de Claude

O Lean, um programa de verificação de provas utilizado por matemáticos em todo o mundo, validou uma formalização completa do Último Teorema de Fermat. Produzido pelo sistema Claude, da Anthropic, e publicado num repositório aberto, o projeto não contém etapas provisórias por resolver, axiomas adicionais nem atalhos computacionais para além dos fundamentos habituais do Lean (repositório). Kevin Buzzard, matemático do Imperial College London que dirigia uma iniciativa própria para formalizar o teorema, compilou o projeto de forma independente e confirmou a validade da prova, classificando-a como «um feito extraordinário de autoformalização» (Buzzard).

A questão matemática estava resolvida há muito: Andrew Wiles demonstrou o teorema em 1995 e o resultado não suscitava dúvidas sérias entre os matemáticos. Faltava converter a demonstração num conjunto de instruções que um verificador literal pudesse processar, incluindo todas as definições e etapas intermédias que um autor humano pode deixar implícitas. Segundo a Anthropic, dezenas de agentes de inteligência artificial fizeram essa conversão em onze dias, durante o mês de agosto, trabalhando em paralelo através de uma plataforma chamada Prove2Me (Anthropic).

Esse prazo, porém, refere-se a um processo que terceiros não conseguem reproduzir: nem o modelo interno, nem a infraestrutura de coordenação, nem as decisões dos operadores, nem os recursos computacionais utilizados foram incluídos na publicação. É possível reproduzir a verificação do resultado final, dado que qualquer pessoa com equipamento suficiente pode voltar a compilar o projeto no Lean e confirmar que a prova é aceite. Um segundo verificador, escrito em Rust pela Anthropic, analisou o mesmo artefacto formal e confirmou a consistência das suas 1 052 234 declarações (relatório técnico). Trata-se de uma nova leitura do mesmo texto formal, e não de uma reconstrução independente da campanha de onze dias.

Como trabalharam os agentes

Formalizar uma demonstração consiste em reescrever o raciocínio do matemático de modo que um programa, desprovido de intuição matemática, consiga validar cada passo lógico. O enunciado parece simples: para qualquer expoente inteiro igual ou superior a três, não existem três números inteiros positivos que satisfaçam aⁿ + bⁿ = cⁿ. A demonstração, pelo contrário, atravessa áreas profundas da teoria dos números e estende-se por centenas de páginas.

O Claude não descobriu matemática nova. Formalizou a cadeia de resultados já conhecida que conduz à prova de Wiles, seguindo uma exposição dos matemáticos Henri Darmon, Fred Diamond e Richard Taylor (Anthropic, relatório técnico). A descoberta intelectual pertenceu a Wiles e aos investigadores que o precederam; o contributo do Claude consistiu em converter esse conhecimento em cerca de 10,5 milhões de linhas de código verificável por máquina (relatório técnico).

A plataforma Prove2Me, concebida pelo investigador da Anthropic Tianyi Peng em colaboração com investigadores da Columbia University, dividiu a demonstração num grafo de dependências com cerca de 29 511 proposições autónomas (relatório técnico). Os agentes escolhiam as proposições cujas dependências já estavam resolvidas, escreviam as respetivas provas em Lean e verificavam os enunciados propostos por outros agentes, o que permitiu executar grande parte do trabalho em paralelo. A operação consumiu aproximadamente seis mil milhões de tokens de saída de um modelo interno de investigação (relatório técnico).

De acordo com a Anthropic, os operadores humanos não escreveram código Lean durante a execução, embora tenham escolhido o teorema, fornecido o percurso conhecido da demonstração, concebido a infraestrutura de agentes e ajustado ocasionalmente as prioridades (Anthropic). A empresa não divulgou a transcrição integral da intervenção dos operadores nem os custos computacionais.

Assente em anos de trabalho humano

O resultado dependeu da Mathlib, a extensa biblioteca de matemática formalizada mantida pela comunidade, e aproveitou diretamente dois projetos anteriores. Desde o final de 2023, a equipa de Buzzard no Imperial construía uma formalização do Último Teorema de Fermat em Lean, apoiada por uma bolsa de um milhão de libras do EPSRC com financiamento previsto até 2029 (bolsa do EPSRC). Outro projeto comunitário já formalizara o teorema para um subconjunto dos casos. O ficheiro de atribuição da Anthropic identifica 106 ficheiros com material retirado ou adaptado destas iniciativas (atribuição).

A execução em paralelo impede uma comparação direta entre os onze dias de calendário e as horas de trabalho humano investidas pela equipa de Buzzard, cujo projeto acumulava cerca de 22 meses de financiamento quando começou a operação do Claude (bolsa do EPSRC). A Anthropic não revelou o número de horas de processamento em unidades gráficas nem o consumo de energia.

Antes desta publicação, o Último Teorema de Fermat era o único elemento ainda por formalizar na lista de Freek Wiedijk de 100 teoremas importantes, uma referência utilizada há duas décadas para acompanhar os avanços neste domínio (Buzzard).

A capacidade de generalizar este método medir-se-á melhor na formalização de matemática recente e menos documentada, para a qual não existam um roteiro detalhado, bibliotecas maduras ou trabalho formal anterior. Neste caso, o sistema recebeu um teorema célebre e uma infraestrutura substancial já construída. O resultado demonstra que agentes de inteligência artificial, quando dispõem de uma via de demonstração conhecida e de trabalho formal prévio, conseguem produzir uma formalização completa que o Lean aceita e que terceiros podem voltar a verificar. Os elementos publicados, contudo, continuam a ser insuficientes para reproduzir o processo que a gerou.