Bolzano prueba 3.800 problemas y detalla cuatro confirmaciones

Qué es Bolzano, y cuándo pasó cada cosa

Bolzano no es un modelo: es la capa que va encima. Reparte papeles entre varias llamadas a un modelo de lenguaje —un demostrador propone, un verificador critica y decide qué se guarda, un sumarizador cierra la ronda— y mantiene el estado de la investigación en tres ficheros Markdown legibles por una persona. Solo el verificador escribe en ese estado: los demostradores proponen y no pisan nada.

El artículo se envió a arXiv el 7 de octubre de 2026, pero esa es la fecha del texto, no la del hallazgo: los cuatro resultados confirmados los dieron por buenos los autores de los artículos de origen, en correspondencia privada, en junio y julio de 2026. Lo firman ocho investigadores de la Universidad Carolina de Praga, la universidad pública más antigua de Europa central; uno de ellos, Pavel Hubáček, está además en el Instituto de Matemáticas de la Academia Checa de Ciencias. La financiación declarada es pública y checa, y no consta aportación de ninguna empresa de IA.

El motor, en cambio, no es suyo: los dos únicos modelos que el artículo dice haber usado son GPT-5.5 y GPT-5.6 Sol, de OpenAI. Lo del equipo es el método, no la máquina que razona. Se presentan además como sistema de código abierto, aunque el artículo no da licencia ni repositorio —la CC BY-SA 4.0 es la del texto— y su única dirección propia es bolzano.app. Los metadatos lo dan como aceptado en el sexto taller MATH-AI de NeurIPS 2026; el documento consultado no describe el proceso de revisión de ese taller.

Las cuatro colecciones y lo que salió de cada una

La extracción no la hizo Bolzano: la hizo otro montaje de agentes, este sí con acceso a los ficheros de los artículos y a búsqueda web, que localizaban los problemas enunciados de forma explícita y miraban si seguían abiertos. Cada problema extraído abrió una investigación propia con un presupuesto fijo de rondas.

En la resolución pasó lo contrario, y a propósito: los tres agentes trabajaron «sin búsqueda web, ejecución de código, acceso directo al sistema de ficheros ni herramienta alguna», para medir lo que los autores llaman «razonamiento puro».

Una precisión que la arquitectura invita a confundir: admite varios demostradores en paralelo, pero los experimentos no fueron así. La nota al pie de la tabla dice que todas las ejecuciones usaron «un solo demostrador», al máximo esfuerzo de razonamiento del modelo.

Leer más: arXiv — Bolzano: From Expert-Guided Proof Search to Automated Open-Problem Solving, Zámečník et al. (7 de octubre de 2026) ↗

Aquí «resuelto» no quiere decir comprobado

La frase que lo decide todo está en el apartado sobre el alcance de la verificación: «El verificador es otro modelo de lenguaje, no un comprobador formal de demostraciones». Un lema aceptado pero incorrecto puede propagarse por la memoria persistente y repetirse después «con una confianza creciente». De ahí su propia conclusión: los documentos de Bolzano «siguen siendo matemáticas candidatas hasta que las comprueba una persona o un sistema formal».

En todo el artículo no hay una sola mención a Lean, Coq o Isabelle, ni a la biblioteca Mathlib, herramientas para formalizar y comprobar demostraciones. La cadena real es otra: verificador que también es un modelo, cribado y auditoría hechos igualmente con modelos, revisión humana y, en cuatro casos, confirmación de los autores del artículo de origen. La auditoría exige que el problema esté «respaldado por la fuente en su lectura prevista» y la demostración sea «sustancialmente correcta»; aprobarla no es resolver, porque «puede describir un avance parcial sustancial».

Los cuatro que sus propios dueños dieron por buenos

De la colección de STOC 2026 —el Symposium on Theory of Computing, el congreso de referencia en teoría de la computación— eligieron cuatro resultados y los mandaron a los autores de los artículos de origen, que los confirmaron en junio y julio de 2026. Algunos piensan incluirlos en sus versiones revisadas.

El primero es un algoritmo de una sola pasada que detecta una biclique plantada semialeatoria con O(log n) bits de memoria cuando los dos lados miden al menos Cn^(2/3): iguala la cota inferior conocida salvo factores logarítmicos. El segundo, una separación exponencial entre programas de rango monótonos y programas de span monótonos.

El tercero, un polinomio cuártico fuertemente convexo en dos variables, con coeficientes racionales, cuyo conjunto de subnivel cero es un solo punto irracional: factibilidad con solución pero sin testigo racional. El cuarto, una cota inferior Ω(log n) de profundidad de circuito para unir dos estados CAT sesgados y para partir uno en dos, incluido el caso de entropía equilibrada que el artículo de origen dejaba abierto.

El matiz va en una nota al pie: en los dos últimos —cuárticas convexas y estados CAT sesgados— «los autores revisaron solo la idea principal, no la demostración completa». De los cuatro confirmados, dos lo están solo en su idea central.

Lo que los autores dicen que les salió mal

Los fallos los enumeran ellos: «hipótesis que faltan, demostraciones que responden a versiones más débiles de las preguntas originales, argumentos no válidos y redescubrimientos de resultados conocidos». No dan cuántos, así que la proporción de falsos positivos no consta. Y el cribado puede dejar escapar salidas útiles: lo que no quedó marcado tampoco puede darse por no resuelto.

Hay tres límites más, y todos son suyos. Su competencia no cubre todos los campos implicados. Los protocolos de cribado y auditoría cambiaron a lo largo de los experimentos, así que las cuatro tandas no se midieron con la misma vara. Y el más incómodo: no hay comparación con el uso directo de los modelos subyacentes; nadie comprobó si GPT-5.5 y GPT-5.6 Sol, a secas y sin Bolzano, habrían llegado a lo mismo.