Illinois reúne 12 151 problemas abiertos y comprueba si la IA puede resolverlos

Un equipo de la Universidad de Illinois en Urbana-Champaign ha presentado OpenFrontiers: un catálogo de 12 151 problemas científicos abiertos y un test de 200 problemas matemáticos. El test responde a una pregunta sencilla: ¿es capaz un agente de IA de redescubrir una solución que la ciencia acaba de conocer? El agente ve los problemas tal como se formulaban antes de resolverse. La respuesta no la comprueba una persona, sino un programa verificador. El resultado es poco alentador para quienes sostienen que «la IA ya está haciendo avanzar la ciencia»: en el modo sin internet, el mejor resultado fue de 7 problemas resueltos de 40.

El mapa de lo no resuelto: qué contiene el catálogo

Hasta ahora, los problemas abiertos estaban dispersos en listas de conferencias, páginas de premios, blogs y secciones de artículos de revisión. Cada fuente tiene sus propias reglas: cómo formular, cómo marcar el estado y bajo qué licencia almacenar. Los autores unificaron 71 fuentes en un único esquema; 62 de ellas aportaron los textos de los problemas. Otros 4 751 registros quedaron en el catálogo como índice, solo con enlaces.

Qué hay en el corpus:

• 11 349 registros (93,4%) son de matemáticas. Les siguen física (339), informática (285) y aprendizaje automático (70). • La mayor concentración de problemas está en teoría de números (2 867) y en geometría y topología (2 371). • Las fuentes más grandes son TheoremDB (3 909), las listas del American Institute of Mathematics (3 470) y el proyecto Formal Conjectures (459). • El 65,9% de los registros tiene código de la clasificación MSC 2020, de uso general en matemáticas. • Solo 1 946 registros, el 16%, tienen enunciado en Lean 4. Lean es un lenguaje en el que la demostración se escribe de modo que el ordenador verifica cada paso.

Los autores no maquillan el estado de los problemas. En el 46% de los registros figura como indeterminado: la fuente simplemente no indica si el problema está resuelto hoy. No se eliminaron los duplicados, para no reescribir enunciados ajenos.

Cómo funciona el test y por qué la «fecha de corte» no basta

OpenFrontiers-Bench consta de dos partes. Rediscovery-110 incluye 110 problemas que estaban abiertos antes de 2026 y que después recibieron una solución. Todas las pruebas de esas soluciones son posteriores al 5 de enero de 2026. Open-90 incluye 90 problemas que siguen sin resolverse. Para 85 problemas resueltos existe una demostración verificada en Lean o un certificado finito exacto, por ejemplo un contraejemplo recalculado con aritmética exacta.

Cada uno de los 200 problemas tiene su enunciado en Lean 4 (versión 4.33.1, biblioteca Mathlib). De los enunciados, 93 se tomaron literalmente de Formal Conjectures, 47 se adaptaron y 60 se escribieron desde cero. Cada enunciado pasó por dos revisores: uno lo cotejaba con el planteamiento original y el otro intentaba romper su sentido. Ambos revisores son modelos de lenguaje, no matemáticos humanos. No quedaron observaciones críticas; en 23 problemas, las dos revisiones solo arrojaron observaciones menores.

Durante la construcción apareció un detalle incómodo. En 55 de las 110 soluciones, los autores de las fuentes atribuyen la matemática clave a sistemas de IA. Si un modelo del mismo «linaje» generó la solución, no se puede hablar de redescubrimiento. Por eso una fecha de corte no es suficiente: el protocolo excluye esos problemas para cada modelo por separado. El modo principal es closed-book, es decir, trabajo sin acceso a la red.

Qué mostraron los siete agentes

Los agentes se probaron en HQ-50: 50 problemas seleccionados por calidad, de los cuales 40 estaban resueltos. Hubo tres condiciones: sin internet, con una copia congelada del buscador y con la web en vivo. Solo contaba una demostración en Lean aceptada por dos programas verificadores independientes en un entorno aislado (sandbox).

• Sin internet, los agentes resolvieron entre 0 y 7 de los 40 problemas. Se trata sobre todo de tres problemas que los humanos resolvieron con una construcción corta. • Con la web en vivo, el mejor resultado fue de 27 problemas. Casi siempre, el agente empezaba por encontrar una solución publicada. • Nadie cerró ningún problema realmente abierto sin haber encontrado antes una solución. • Los agentes fuertes a menudo se rinden sin agotar su presupuesto de tiempo cuando el problema es demasiado difícil.

Qué implica todo esto

Las mediciones como las olimpiadas y los exámenes con respuesta conocida de antemano ya no distinguen la investigación real de una buena búsqueda. OpenFrontiers muestra cómo separar una de otra: prohibir la red, plantear el problema con su formulación anterior a la resolución y aceptar solo resultados verificados formalmente. Para laboratorios e inversores, es un filtro útil frente a las grandes afirmaciones sobre «científicos de IA». Para los investigadores, es un mapa listo de lo no resuelto y un conjunto de problemas en los que el éxito no puede atribuirse a una filtración de los datos de entrenamiento.

También hay limitaciones. El test es casi por completo matemático, y los enunciados en Lean están disponibles solo para una pequeña parte del corpus. La revisión de los enunciados la hicieron los propios modelos, aunque en dos pasadas independientes. Los datos y el test están publicados en Hugging Face, en la colección FlippyDora/openfrontiers.