Uma demonstração que levou um matemático sete anos para construir, e outro pesquisador um período projetado de cinco anos para formalizar, foi agora concluída por uma equipe de agentes de IA em onze dias. O modelo Claude da Anthropic produziu uma versão formal do Último Teorema de Fermat, um dos problemas mais célebres da história da matemática. Isto não é uma demonstração nova. É algo indiscutivelmente mais útil: uma confirmação legível por máquina e verificada por máquina de que a demonstração humana está correta, construída do zero em uma linguagem de programação chamada Lean.
Um Problema de 350 Anos, e o que “Formalizar” Realmente Significa
O Último Teorema de Fermat afirma que nenhum número inteiro a, b e c pode satisfazer a equação aⁿ + bⁿ = cⁿ quando n é um número inteiro maior do que 2. Pierre de Fermat propôs o enigma no século 17, observando famosamente na margem de um livro didático que havia encontrado uma demonstração, mas faltava espaço para anotá-la. Essa nota assombrou a matemática por cerca de três séculos e meio.
Andrew Wiles finalmente demonstrou o teorema em 1995, após trabalhar no problema em segredo por sete anos. Sua demonstração não foi isenta de dificuldades: uma falha foi descoberta, e levou Wiles e seu colaborador Richard Taylor aproximadamente um ano para consertá-la. O episódio ilustra uma vulnerabilidade estrutural nas demonstrações matemáticas tradicionais. Elas são escritas em linguagem natural e notação lógica, verificadas por especialistas humanos, e vulneráveis a erros que podem se esconder dentro de longas cadeias de raciocínio.
A formalização aborda essa vulnerabilidade diretamente. Ela significa traduzir uma demonstração em código de computador, especificamente em uma linguagem formal que uma máquina pode verificar passo a passo. Não há ambiguidade em código. Ou a lógica se sustenta ou não se sustenta. Um repositório central chamado Mathlib já armazena cerca de 2 milhões de linhas de matemática formalizada. A nova demonstração da Anthropic adiciona 13 milhões de linhas a esse cenário, cobrindo cerca de 29.500 teoremas intermediários que foram necessários para alcançar o resultado final. Isso a torna mais de cinco vezes maior do que todo o conteúdo anterior do Mathlib combinado, e a maior demonstração em Lean já escrita.
Como os Agentes Realmente Trabalharam (e Onde Eles Enfrentaram Dificuldades)
O sistema da Anthropic não usou um único modelo de IA trabalhando isoladamente. Múltiplos agentes separados foram mobilizados, cada um designado para diferentes porções do problema, abordando pedaços menores do teorema em paralelo. O processo funcionou de forma contínua e autônoma por onze dias.
Especialistas humanos não estiveram ausentes. Eles forneceram o que a Anthropic descreve como “instruções de alto nível” para manter o trabalho no caminho certo. Vale a pena notar isso: os agentes periodicamente perderam o controle do estado geral do projeto e pararam de colaborar efetivamente. O sistema exigiu orientação externa para se recuperar dessas falhas. O que ajudou no final foi uma ferramenta originalmente projetada para colaboração matemática humana, chamada Prove2Me. Assim que os agentes começaram a usá-la para rastrear seu trabalho e se coordenar sobre os próximos passos, o projeto avançou de forma mais confiável.
Kevin Buzzard, um matemático do Imperial College London que liderava um projeto de cinco anos para formalizar a mesma demonstração de Wiles e Taylor, comentou sobre o resultado. Ele observou que a demonstração se apoia em “nenhum outro pressuposto além dos axiomas da matemática”, e descreveu o trabalho como sendo de múltiplas camadas, tocando em álgebra, análise harmônica, geometria e teoria dos números. Sua avaliação é significativa: Buzzard não era um espectador. Ele havia organizado uma conferência em Londres no início deste ano reunindo especialistas em IA, cientistas da computação e matemáticos para trabalhar exatamente neste problema. O anúncio da Anthropic atropelou esse esforço por completo.
Por Que Isso Importa Além do Teorema em Si
Aqui está o que a maior parte da cobertura desta história deixa escapar. O teorema em si não é o ponto principal. O Último Teorema de Fermat já havia sido demonstrado. O que a Anthropic demonstrou é algo sobre a natureza do conhecimento matemático e como ele pode ser verificado, estendido e construído a partir daí.
Buzzard colocou isso de forma direta: se a IA agora pode autoformalizar uma demonstração desta complexidade, então a formalização automática da literatura matemática moderna mais ampla se torna uma meta realista de curto prazo. Essa é uma mudança significativa. A matemática é a fundação da física, da criptografia, da ciência da computação e da engenharia. Um corpo de conhecimento matemático formalizado e verificável por máquina permitiria aos pesquisadores construir sobre resultados anteriores com muito mais confiança, capturando erros que a revisão humana pode deixar passar e acelerando o ritmo no qual novos resultados podem ser estabelecidos.
O episódio também ilustra algo importante sobre como os sistemas de IA atualmente operam em trabalhos intelectuais de alto risco. Eles não são autônomos da maneira como a palavra às vezes é usada de forma vaga. Eles exigiram supervisão humana, quebraram durante a coordenação e precisaram de ferramentas projetadas para a colaboração humana para funcionar efetivamente. O cronograma de onze dias é notável. A necessidade de orientação humana do início ao fim é igualmente informativa.
A IA aqui não está substituindo os matemáticos. Ela está lidando com um volume e uma granularidade de verificação lógica que nenhuma equipe humana conseguiria sustentar nesta escala, liberando os pesquisadores para focar nas questões de nível superior sobre o que demonstrar e por que isso importa.
Em Resumo
Os agentes de IA da Anthropic produziram a maior demonstração formal já escrita, verificando o Último Teorema de Fermat em código Lean legível por máquina ao longo de 13 milhões de linhas e 29.500 passos intermediários. O resultado importa menos como uma descoberta matemática e mais como uma demonstração de que a IA agora pode formalizar demonstrações complexas e em camadas a uma escala e velocidade antes fora de alcance. O processo exigiu orientação humana e falhou mais de uma vez. Esse contexto também pertence à história.
Com base em reportagem de New Scientist.