Agentes de IA formalizaram 15 000 páginas de provas em 24 dias e encontraram uma lacuna

Várias dezenas de agentes de IA transformaram, em 24 dias, uma demonstração de cerca de 15 000 páginas em mais de 43 milhões de linhas de código, que o computador verifica passo a passo. Matemáticos de primeira linha trabalharam nesse texto por décadas, e ele é uma das construções mais monumentais da história da matemática. No caminho, o sistema encontrou no raciocínio dos autores uma lacuna lógica que existia havia quase 40 anos.

Uma página de três mil linhas

Formalizar uma demonstração significa escrever de forma explícita cada passo que o matemático, no artigo, pula com a frase "como é fácil verificar". Depois, um programa verificador precisa aceitar esse registro. Se houver um furo na cadeia, o código simplesmente não passa na verificação.

A aritmética mostra a escala. 43 milhões de linhas para 15 000 páginas dão cerca de 2 900 linhas por página. Em 24 dias, isso equivale a algo como 1,8 milhão de linhas por dia, ou cerca de 75 mil por hora, sem parar. Uma equipe humana não daria conta desse volume: formalizar até teoremas pequenos costuma levar meses para especialistas.

Por que foi justamente uma máquina que achou o furo

A lacuna de quase 40 anos sobreviveu a dezenas de leitores atentos. Não foi descuido deles. Verificar 15 000 páginas à mão é inviável: o revisor se apoia na autoridade dos autores e na premissa de que os passos intermediários são suficientemente óbvios. O verificador não concede esse crédito de confiança. Cada transição, ele aceita ou rejeita.

Por isso, a formalização funciona também como auditoria. O agente que tenta codificar um passo esbarra num ponto em que não há justificativa. Para a matemática, é um sinal sério: trata-se da integridade do edifício, e não de um retoque estético.

Economia: quantos tokens custa uma obra dessas

Esta é uma estimativa da redação, não um dado do projeto. Com 10–12 tokens por linha, o código final soma cerca de meio bilhão de tokens de saída. O consumo real é muito maior, porque os agentes escrevem rascunhos, recebem erros do verificador, reescrevem e verificam de novo. Considerando essas iterações, a conta provavelmente chega a bilhões de tokens.

Já o prazo de 24 dias foi alcançado graças ao paralelismo. Uma demonstração grande se decompõe naturalmente em um grafo de lemas com dependências, e os ramos independentes podem ser entregues a agentes diferentes ao mesmo tempo. O verificador atua como árbitro com resposta binária, "aceito ou não", de modo que os agentes não precisam confiar uns nos outros na palavra.

Principais números do projeto:

• cerca de 15 000 páginas da demonstração original, construída ao longo de décadas;
• 24 dias de trabalho do sistema;
• várias dezenas de agentes trabalhando em paralelo;
• mais de 43 milhões de linhas de código verificável;
• cerca de 1,8 milhão de linhas por dia, em média;
• cerca de 2 900 linhas de código por página de texto;
• uma lacuna na argumentação com quase 40 anos.

O que dá para levar daqui para a prática de engenharia

A principal lição vale para além da matemática. Sistemas de agentes escalam melhor onde existe um verificador automático inequívoco: compilador, conjunto de testes, motor de provas. Nesse cenário, centenas de milhares de linhas geradas não exigem revisão manual, porque a 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 sempre as mesmas: especificação detalhada, verificador rígido e possibilidade de dividir o trabalho em partes independentes. Para equipes que planejam pipelines de agentes, a conclusão prática é esta: vale começar investindo no verificador e na decomposição da tarefa, enquanto o número de agentes e o tamanho do modelo vêm em segundo plano. Há ainda uma conclusão para a revisão por pares: uma demonstração formalizada oferece uma garantia reproduzível que um texto manuscrito de 15 000 páginas não consegue oferecer.