Agentes de IA traduziram uma prova de 15 mil páginas em 43 milhões de linhas de código em 24 dias — e encontraram um erro de 40 anos

Traduzir uma montanha de matemática para algo que uma máquina possa checar

Uma equipe de várias dezenas de agentes de IA passou 24 dias reescrevendo uma das provas matemáticas mais extensas da história — cerca de 15 mil páginas de texto nas quais os principais matemáticos trabalharam durante décadas — em um formato compreensível para um computador: mais de 43 milhões de linhas de código, verificadas passo a passo por um programa verificador. No processo, os agentes descobriram uma lacuna lógica no raciocínio que havia passado despercebida por quase 40 anos.

O que significa "formalizar" uma prova

Um artigo matemático convencional é escrito para humanos e está repleto de frases como "é fácil ver que" ou "é evidente que" — o autor pula etapas intermediárias, confiando que um leitor especialista vai reconstruí-las por conta própria. A formalização exige escrever explicitamente cada uma dessas etapas, sem lacunas, como código que depois é verificado por um programa dedicado. Se houver um buraco em algum ponto da cadeia de raciocínio, o código simplesmente não passa pela verificação — não há meio-termo aqui.

A escala da operação fica clara em uma conta simples: 43 milhões de linhas de código para um documento-fonte de 15 mil páginas equivalem a cerca de 2.900 linhas por página de texto. Em 24 dias de trabalho, isso dá aproximadamente 1,8 milhão de linhas por dia, ou cerca de 75 mil linhas por hora de trabalho ininterrupto. Para comparação, formalizar manualmente até teoremas de tamanho modesto costuma levar meses para especialistas humanos — um volume que uma equipe de matemáticos jamais conseguiria enfrentar à mão.

Por que foi uma máquina, e não humanos, que encontrou a brecha na prova

A lacuna no raciocínio encontrada pelos agentes sobreviveu a dezenas de revisores atentos durante quase 40 anos. Isso não indica descuido por parte dessas pessoas — é consequência da própria natureza da revisão manual. Ler 15 mil páginas do início ao fim e reconferir cada transição lógica é algo fisicamente inviável. Um revisor inevitavelmente se apoia na reputação dos autores e na sensação intuitiva de que um determinado passo "parece correto".

O verificador simplesmente não tem essa confiança disponível. Qualquer transição de uma afirmação para outra é aceita como rigorosamente demonstrada ou rejeitada. Quando um agente de IA tenta codificar o próximo passo da prova, mais cedo ou mais tarde encontra um ponto onde falta justificativa — e, a partir daí, o código simplesmente não compila. Para a comunidade matemática, isso é um sinal sério, não uma objeção formal: está em jogo a integridade de toda uma construção considerada concluída havia décadas.

Quanto isso custa em tokens

Esta é uma estimativa da redação do Hamidun News, não dados oficiais do projeto. Considerando de 10 a 12 tokens por linha de código final, os 43 milhões de linhas resultantes equivalem a cerca de meio bilhão de tokens só na saída final. O consumo real é bem maior: os agentes escrevem versões preliminares, recebem erros do verificador, reescrevem trechos e repetem a verificação. Levando em conta todas essas iterações, o total provavelmente já está na faixa de bilhões de tokens.

O prazo curto de 24 dias só foi possível graças ao trabalho em paralelo. Uma prova grande se decompõe naturalmente em um grafo de lemas com dependências entre si, e os ramos independentes desse grafo podem ser distribuídos simultaneamente entre diferentes agentes. O verificador, por sua vez, atua como um árbitro imparcial com resposta binária de "aprovado" ou "rejeitado" — por isso os agentes não precisam confiar na palavra uns dos outros: qualquer trecho de código passa pela verificação ou não passa.

O que equipes de engenharia podem aproveitar disso

A principal lição não se limita à matemática pura. Sistemas agênticos escalam melhor onde existe um juiz automático inequívoco: um compilador, uma suíte de testes ou um motor de prova. Nessas condições, centenas de milhares de linhas de código geradas não precisam ser revisadas manualmente — a própria máquina faz a triagem.

O mesmo esquema se aplica à verificação formal de bibliotecas criptográficas, compiladores, protocolos de consenso e blocos de hardware. As condições são as mesmas em todos os casos: uma especificação detalhada da tarefa, um verificador automático rigoroso e a possibilidade de dividir o trabalho em blocos independentes. Equipes que planejam construir pipelines agênticos semelhantes devem investir principalmente no próprio verificador e na decomposição da tarefa em unidades independentes — o número de agentes e o tamanho do modelo são secundários aqui. Uma última conclusão prática envolve a revisão por pares: uma prova formalizada oferece uma garantia reproduzível de correção que um texto manuscrito de 15 mil páginas simplesmente não pode fornecer.