Bolzano prova 3.800 problemes oberts i en detalla quatre de confirmats

Què és Bolzano, i quan va passar cada cosa

Bolzano no és un model: és la capa que hi va al damunt. Reparteix papers entre diverses crides a un model de llenguatge —un demostrador proposa, un verificador critica i decideix què es desa, un sumaritzador tanca la ronda— i manté l'estat de la recerca en tres fitxers Markdown llegibles per una persona. Només el verificador escriu en aquest estat: els demostradors proposen i no trepitgen res.

L'article es va enviar a arXiv el 7 d'octubre de 2026, però aquesta és la data del text, no la de la troballa: els quatre resultats confirmats els van donar per bons els autors dels articles d'origen, en correspondència privada, al juny i al juliol de 2026. El signen vuit investigadors de la Universitat Carolina de Praga, la universitat pública més antiga de l'Europa central; un d'ells, Pavel Hubáček, és també a l'Institut de Matemàtiques de l'Acadèmia Txeca de Ciències. El finançament declarat és públic i txec, i no hi consta l'aportació de cap empresa d'IA.

El motor, en canvi, no és seu: els dos únics models que l'article diu haver fet servir són GPT-5.5 i GPT-5.6 Sol, d'OpenAI. El que és de l'equip és el mètode, no la màquina que raona. Es presenten, a més, com a sistema de codi obert, tot i que l'article no dona llicència ni repositori —la CC BY-SA 4.0 és la del text— i la seva única adreça pròpia és bolzano.app. Les metadades el donen com a acceptat al sisè taller MATH-AI de NeurIPS 2026; el document consultat no descriu el procés de revisió d'aquest taller.

Les quatre col·leccions i què va sortir de cadascuna

L'extracció no la va fer Bolzano: la va fer un altre muntatge d'agents, aquest sí amb accés als fitxers dels articles i a cerca web, que localitzaven els problemes enunciats de manera explícita i miraven si continuaven oberts. Cada problema extret va obrir una recerca pròpia amb un pressupost fix de rondes.

En la resolució va passar el contrari, i expressament: els tres agents van treballar «sense cerca web, execució de codi, accés directe al sistema de fitxers ni cap eina», per mesurar el que els autors anomenen «raonament pur».

Un matís que l'arquitectura convida a confondre: admet diversos demostradors en paral·lel, però els experiments no van ser així. La nota al peu de la taula diu que totes les execucions van fer servir «un sol demostrador», al màxim esforç de raonament del model.

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

Aquí «resolt» no vol dir comprovat

La frase que ho decideix tot és a l'apartat sobre l'abast de la verificació: «El verificador és un altre model de llenguatge, no un comprovador formal de demostracions». Un lema acceptat però incorrecte es pot propagar per la memòria persistent i repetir-se després «amb una confiança creixent». D'aquí la seva pròpia conclusió: els documents de Bolzano «continuen sent matemàtiques candidates fins que les comprova una persona o un sistema formal».

En tot l'article no hi ha ni una sola menció a Lean, Coq o Isabelle, ni a la biblioteca Mathlib, eines per formalitzar i comprovar demostracions. La cadena real és una altra: un verificador que també és un model, un cribratge i una auditoria fets igualment amb models, revisió humana i, en quatre casos, confirmació dels autors de l'article d'origen. L'auditoria exigeix que el problema estigui «avalat per la font en la lectura prevista» i que la demostració sigui «substancialment correcta»; aprovar-la no és resoldre, perquè «pot descriure un avenç parcial substancial».

Els quatre que els seus propis amos van donar per bons

De la col·lecció de STOC 2026 —el Symposium on Theory of Computing, el congrés de referència en teoria de la computació— en van triar quatre resultats i els van enviar als autors dels articles d'origen, que els van confirmar al juny i al juliol de 2026. Alguns pensen incloure'ls en les versions revisades.

El primer és un algorisme d'una sola passada que detecta una biclique plantada semialeatòria amb O(log n) bits de memòria quan els dos costats mesuren almenys Cn^(2/3): iguala la fita inferior coneguda llevat de factors logarítmics. El segon, una separació exponencial entre programes de rang monòtons i programes de span monòtons.

El tercer, un polinomi quàrtic fortament convex en dues variables, amb coeficients racionals, el conjunt de subnivell zero del qual és un sol punt irracional: factibilitat amb solució però sense testimoni racional. El quart, una fita inferior Ω(log n) de profunditat de circuit per unir dos estats CAT esbiaixats i per partir-ne un en dos, inclòs el cas d'entropia equilibrada que l'article d'origen deixava obert.

El matís va en una nota al peu: en els dos últims —quàrtiques convexes i estats CAT esbiaixats— «els autors només van revisar la idea principal, no la demostració completa». Dels quatre confirmats, dos ho estan només en la idea central.

El que els autors diuen que els va sortir malament

Les errades les enumeren ells: «hipòtesis que falten, demostracions que responen a versions més febles de les preguntes originals, arguments no vàlids i redescobriments de resultats coneguts». No en donen el nombre, així que la proporció de falsos positius no consta. I el cribratge pot deixar escapar sortides útils: el que no es va marcar tampoc no es pot donar per no resolt.

Hi ha tres límits més, i tots són seus. La seva competència no cobreix tots els camps implicats. Els protocols de cribratge i auditoria van canviar al llarg dels experiments, de manera que les quatre tandes no es van mesurar amb la mateixa vara. I el més incòmode: no hi ha comparació amb l'ús directe dels models subjacents; ningú no va comprovar si GPT-5.5 i GPT-5.6 Sol, tot sols i sense Bolzano, haurien arribat al mateix.