Sistema de IA sem treinamento adicional resolveu os 6 problemas da IMO 2026 em Lean

Pesquisadores da Case Western Reserve University (o trabalho foi feito durante um estágio na Amazon Web Services) mostraram que um grande modelo de linguagem pronto, sem nenhum treinamento adicional, consegue provar teoremas complexos e a correção de programas, desde que o trabalho ao redor dele seja bem organizado. Eles usaram o Anthropic Fable-5. As provas são escritas em Lean, uma linguagem em que um pequeno «kernel» verifica cada passo do raciocínio e não pode ser enganado.

O sistema resolveu os seis problemas formalizados da Olimpíada Internacional de Matemática de 2026. Também passou em todas as tarefas do VERINA (conjunto de programação verificada) e lidou com as condições de verificação do NTP4VC, um conjunto industrial de verificação formal de código. Além disso, resolve problemas do PutnamBench, conjunto de tarefas formalizadas da olimpíada universitária Putnam.

Cada resultado contabilizado é a prova ou a refutação de um enunciado, e ambas foram verificadas pelo kernel do Lean.

Uma árvore de agentes em vez de uma série de reinícios

A dificuldade é que o Lean responde apenas a uma pergunta local: se determinado passo passa ou não. Uma divisão ruim do problema em partes, ou um lema (afirmação auxiliar) que está faltando, só aparece depois de dezenas de passos. Além disso, o modelo é limitado pela janela de contexto e pelo orçamento de computação.

Os autores resolvem isso de forma recursiva. O agente principal lança agentes filhos, e cada um busca uma estratégia de prova diferente ou o lema necessário. O funcionamento é este:

• cada filho tem um contexto limpo e uma cópia própria do projeto; • um filho pode gerar seus próprios filhos, e as ferramentas são as mesmas para todos; • um filho pode gastar dezenas de chamadas em um único lema, mas devolve ao pai apenas o lema pronto, um contraexemplo ou achados parciais; • os resultados chegam ao pai no turno seguinte, sem esperar as outras ramificações, de modo que uma descoberta antecipada pode redirecionar a busca; • a busca termina quando a primeira prova adequada é aceita.

O espírito lembra a busca em árvore de Monte Carlo, mas as decisões são tomadas pelo próprio modelo. Ele lê o conteúdo das respostas dos filhos e escolhe sozinho quais ramificações continuar, alterar ou expandir. Contadores de visitas e estimativas médias não são usados.

Outra ferramenta é o teste paralelo de táticas. O agente lança vários candidatos de uma só vez sobre o estado atual da prova. A tática que funciona volta ao contexto, e os rastros das tentativas fracassadas são descartados, para que o contexto não fique poluído.

Lean como serviço escalável

As provas mais difíceis exigiram dezenas de subagentes em uma única execução. Uma máquina só não tinha poder suficiente para o Lean, então a verificação foi movida para um serviço separado e sem estado. Os clientes enviam o código-fonte Lean por JSON-RPC, em vez de apontar para arquivos locais. Qualquer réplica disponível, com as mesmas versões de Lean e Mathlib, pode processar qualquer requisição.

Dentro de cada réplica há um pool de processos de trabalho com a biblioteca Mathlib já carregada. A importação leva dezenas de segundos, por isso os processos são reaproveitados, e a verificação em um processo «quente» é bem mais rápida. As réplicas rodam em Kubernetes, e o número delas se ajusta automaticamente à carga.

Há ainda uma proteção específica contra trapaça. Um agente que edita o arquivo da prova poderia enfraquecer o enunciado do teorema, deixar um placeholder sorry ou adicionar um axioma. Por isso, tudo até a assinatura do teorema fica congelado, e a verificação final é feita pelo Lean Comparator: o arquivo deve compilar sem placeholders e usar apenas os axiomas permitidos. O relatório de sucesso do próprio agente não é levado em conta.

Um novo exame: código de olimpíada como tarefa de verificação

Os testes antigos estão quase esgotados, e os conjuntos escritos à mão para verificação de código são pequenos: têm centenas de tarefas, que podem ser memorizadas ou encontradas nos dados de treinamento. Por isso, os autores construíram um pipeline que gera as tarefas automaticamente:

• um agente programador escreve soluções seguras em Rust para problemas no estilo LeetCode, com uma única função pura sobre dados simples (números, listas, strings, árvores, listas encadeadas); • a solução passa por testes de referência e depois é traduzida para um modelo executável em Lean; • Rust e Lean rodam sobre as mesmas entradas, e só são aceitos os programas cujas saídas coincidem por completo; • outro agente escreve a especificação, isto é, a propriedade que deve ser satisfeita ou violada; • o enunciado é congelado, e o provador o prova ou o refuta.

A diferença em relação aos conjuntos escritos à mão é que as tarefas trazem obrigações no nível da implementação: aritmética de largura fixa, erros explícitos, laços gerados, conversões de tipo e a substituição funcional de estado mutável. As refutações geram rótulos negativos, que não existem em pipelines só com provas. A especificação é escrita por outro agente antes de o provador vê-la, e o provador não pode escolher um enunciado mais fácil.

Em uma amostra de enunciados, com limite de 30 minutos para cada um, o sistema resolve apenas uma parte. Para um provador que quase esgotou os benchmarks antigos, as tarefas continuam longe da saturação. Elas podem ser escaladas com computação, usadas para comparar outros provadores e servir como recompensas em aprendizado por reforço com recompensas verificáveis (RLVR). O teste de código não «adivinha» nada: entrega um veredito verificável do kernel. Mutações de programas (pequenas alterações em código correto) geram tarefas adicionais com rótulos negativos, mas o artigo não as avalia.

O que isso muda para engenheiros

A principal conclusão prática: sem treinamento adicional, é possível concentrar o esforço na infraestrutura ao redor do modelo. Isolamento de contextos, busca assíncrona, testes paralelos e um serviço de verificação elástico permitem que um modelo comum extraia do Lean um resultado que antes exigia modelos treinados especificamente, como o Goedel-Code-Prover. Quem constrói agentes de verificação de código também pode aproveitar o esquema com enunciado congelado e verificação final independente: ele fecha as formas típicas de enganar o verificador.