Universidade de Illinois reúne 12 151 problemas abertos e testa se a IA consegue resolvê-los

Uma equipe da Universidade de Illinois em Urbana-Champaign lançou o OpenFrontiers: um catálogo com 12 151 problemas científicos abertos e um teste com 200 problemas de matemática. O teste responde a uma pergunta simples: um agente de IA consegue redescobrir uma solução que acabou de se tornar conhecida pela ciência? O agente vê os problemas na forma em que eram formulados antes de serem resolvidos. Quem confere a resposta não é uma pessoa, mas um programa verificador. O resultado é desanimador para quem defende que "a IA já está impulsionando a ciência": no modo sem internet, o melhor desempenho foi de 7 problemas resolvidos em 40.

Mapa do que está em aberto: o que há no catálogo

Até agora, os problemas abertos estavam espalhados por listas de conferências, páginas de prêmios, blogs e seções de artigos de revisão. Cada fonte tem suas próprias regras: como formular o problema, como marcar o status, sob qual licença armazenar. Os autores reuniram 71 fontes em um esquema único, e 62 delas forneceram os textos dos problemas. Outros 4 751 registros ficaram no catálogo apenas como índice, só com links.

O que há no corpus:

• 11 349 registros (93,4%) são de matemática. Em seguida vêm física (339), ciência da computação (285) e aprendizado de máquina (70). • A maior parte dos problemas está em teoria dos números (2 867) e em geometria e topologia (2 371). • As maiores fontes são TheoremDB (3 909), as listas do American Institute of Mathematics (3 470) e o projeto Formal Conjectures (459). • 65,9% dos registros têm código da classificação MSC 2020, adotada na matemática. • Só 1 946 registros, ou 16%, têm enunciado em Lean 4. Lean é uma linguagem em que a demonstração é escrita de modo que o computador verifica cada passo.

Os autores não maquiam o status dos problemas. Em 46% dos registros ele está marcado como indefinido: a fonte simplesmente não informa se o problema foi resolvido até hoje. Os duplicados não foram removidos, para não reescrever enunciados alheios.

Como o teste funciona e por que a "data de corte" não resolve

O OpenFrontiers-Bench tem duas partes. O Rediscovery-110 reúne 110 problemas que estavam abertos antes de 2026 e depois receberam uma solução. Todas as evidências de solução são posteriores a 5 de janeiro de 2026. O Open-90 reúne 90 problemas que continuam sem solução. Para 85 dos problemas resolvidos, há uma demonstração verificada em Lean ou um certificado finito exato, por exemplo um contraexemplo recalculado com aritmética exata.

Cada um dos 200 problemas tem enunciado em Lean 4 (versão 4.33.1, biblioteca Mathlib). Dos enunciados, 93 foram copiados literalmente do Formal Conjectures, 47 foram adaptados e 60 foram escritos do zero. Cada enunciado passou por dois revisores: um o comparava com o problema original, e o outro tentava quebrar o seu sentido. Os dois revisores são modelos de linguagem, não matemáticos humanos. Não restaram observações críticas, e em 23 problemas as duas revisões apontaram apenas observações menores.

Na montagem, apareceu um detalhe incômodo. Em 55 das 110 soluções, os autores das fontes atribuem a matemática central a sistemas de IA. Se um modelo da mesma "linhagem" gerou a solução, não dá para falar em redescoberta. Por isso, a data de corte sozinha não basta: o protocolo exclui esses problemas para cada modelo separadamente. O modo principal é o closed-book, ou seja, trabalho sem acesso à rede.

O que os sete agentes mostraram

Os agentes foram testados no HQ-50: 50 problemas selecionados por qualidade, dos quais 40 já resolvidos. Foram três condições: sem internet, com uma cópia congelada de buscas e com a web ao vivo. Só valia a demonstração em Lean aceita por dois programas verificadores independentes, em um ambiente isolado (sandbox).

• Sem internet, os agentes resolveram de 0 a 7 dos 40 problemas. Na maior parte, são três problemas que humanos resolveram com uma construção curta. • Com a web ao vivo, o melhor resultado foi de 27 problemas. Quase sempre o agente começava encontrando uma solução publicada. • Nenhum agente resolveu um problema realmente aberto sem ter encontrado uma solução pronta. • Agentes fortes costumam desistir sem esgotar o orçamento de tempo quando o problema é difícil demais.

O que isso significa

Testes como olimpíadas e provas com resposta previamente conhecida já não distinguem pesquisa de verdade de uma boa busca. O OpenFrontiers mostra como separar uma coisa da outra: proibir a rede, apresentar o problema na formulação de antes da solução e aceitar apenas resultados verificados formalmente. Para laboratórios e investidores, é um filtro útil contra declarações bombásticas sobre "cientistas de IA". Para pesquisadores, é um mapa pronto do que está em aberto e um conjunto de problemas em que o sucesso não pode ser atribuído a vazamento de dados de treinamento.

Há também limitações. O teste é quase todo de matemática, e os enunciados em Lean existem para uma pequena parte do corpus. A verificação dos enunciados foi feita pelos próprios modelos, embora em duas passagens independentes. Os dados e o teste estão publicados no Hugging Face, na coleção FlippyDora/openfrontiers.