«Verificat en Lean» no vol dir el que sembla

Publicar no és el mateix que comprovar

Una demostració matemàtica clàssica és un text: algú l'escriu, altres especialistes el llegeixen, segueixen el raonament línia a línia i diuen si s'aguanta. Funciona des de fa segles i té un coll d'ampolla evident, perquè depèn que hi hagi qui s'assegui a llegir-lo, i llegir una demostració llarga pot durar mesos.

El 6 d'octubre de 2026, OpenAI va publicar de cop 722 manuscrits de matemàtiques sortits d'un model intern sense llançar. Amb aquest volum sobre la taula, una distinció que solia quedar entre especialistes passa a ser el primer de tot: publicar un resultat i comprovar-lo són dues coses diferents.

I convé no barrejar les etiquetes: «publicat en un repositori», «formalitzat en Lean» i «revisat per altres matemàtics» diuen tres coses diferents, i cap de les tres no implica les altres dues.

Lean no llegeix prosa: comprova passos

Lean és un llenguatge d'ordinador pensat per escriure matemàtiques. No admet prosa: cada pas es declara i s'ha de derivar dels anteriors amb regles que el programa coneix. Si tot encaixa, Lean ho accepta; si un pas no se segueix de l'anterior, el rebutja i diu en quina línia es trenca la cadena.

Aquí hi ha la gràcia i també el límit. Un «sí» de Lean és una garantia forta i molt estreta: l'argument no té buits lògics. No diu que el resultat sigui interessant, ni nou, ni que l'enunciat demostrat sigui el que importava.

I Lean no llegeix l'article: comprova la versió de l'argument que algú li ha escrit abans en el seu llenguatge. Aquesta feina prèvia explica gairebé tota la resta.

Formalitzar és traduir, i traduir costa

Formalitzar és traduir una demostració de la prosa matemàtica a aquell llenguatge que la màquina verifica. És feina humana, lenta i especialitzada: cada salt implícit s'ha de convertir en passos explícits, recolzant-se en el que la biblioteca de Lean ja té demostrat. Si falta una peça de base, s'ha de demostrar primer.

L'exemple que mesura millor el cost és l'últim teorema de Fermat. La seva formalització en Lean, datada el 5 de setembre de 2026, no es va fer perquè el resultat fos dubtós: estava demostrat i acceptat des de feia dècades. Tot i així va necessitar anys de feina.

D'aquí surt una regla per llegir titulars: que un resultat no estigui formalitzat gairebé mai no vol dir que ningú no se'l cregui, sinó que formalitzar-lo costa i que encara no li ha tocat.

Les tres situacions, i la del mig és la que enganya

Amb això ja es pot ordenar l'assumpte: un resultat publicat pot estar en tres situacions, i aquesta diferència és l'única cosa que cal retenir.

Formalitzada i acceptada és el cas còmode. Formalitzada i rebutjada és l'incòmode, però clar: el programa ha trobat el buit i diu on és, de manera que la demostració, tal com està escrita, no val.

La que es llegeix malament és la del mig. «No formalitzada» vol dir que no està comprovada, no que estigui desmentida: està pendent de revisió, per una persona o per la màquina, i pot tenir problemes o no tenir-ne. És un «encara no», no un «no», i aquí s'hi cola la trampa: «no verificat» es llegeix com «fals».

I de tant en tant en té. El 7 d'octubre de 2026, un dia després de publicar el seu catàleg de manuscrits, OpenAI en va retirar tres: en un, diu el seu propi historial, «un error de signe invalida» un argument, i amb ell queien els altres dos, que feien servir aquesta mateixa construcció. Un error de signe que tomba un pas és justament la mena de buit que un comprovador mecànic no deixa passar: escrit en Lean, aquell pas no compila. L'historial no diu qui va trobar la fallada ni si aquells manuscrits portaven formalització. I el que el cas no fa és moure de casella els altres: els centenars de manuscrits sense formalitzar continuen pendents, que és precisament el que significa la casella del mig.

Un manuscrit és un text que encara no avala ningú

La paraula «article» fa aquí molt de mal, perquè en el llenguatge corrent sona a una cosa ja publicada i aprovada per algú. En matemàtiques, un text pot estar a internet, llegible i fins i tot citat, sense haver passat per cap filtre extern.

Publicar així no té res d'irregular: és el procediment habitual de la disciplina. L'irregular és comptar un manuscrit com si fos un resultat comprovat. Així que la pregunta útil no és «està publicat?», que gairebé sempre ho està, sinó «qui se l'ha mirat, i amb què?».

L'altra manera de comprovar continua sent humana i lenta

Les dues maneres de comprovar no competeixen, fan coses diferents: Lean decideix si l'argument s'aguanta i la revisió per parells decideix si el treball aporta alguna cosa i està ben plantejat. Un resultat pot passar l'una i no l'altra.

Per això un catàleg ple de formalitzacions no tanca l'expedient, ni una revista substitueix la màquina. Amb més de set-cents textos nous de cop, cap de les dues vies no és instantània.

El material del 6 d'octubre, llegit amb aquestes tres etiquetes

El que OpenAI va publicar el 6 d'octubre de 2026 en un repositori públic reunia 722 manuscrits agrupats en 372 famílies, sortits d'uns 4.000 problemes plantejats al model, amb una mitjana de tres hores de càlcul per resultat. Al costat hi anaven una biblioteca de Lean i un catàleg que descriu «les demostracions formals disponibles, els articles associats i les configuracions de verificació».

El que importa aquí és com es descriu el repositori a si mateix. Diu que la col·lecció «inclou resultats en diferents fases de verificació», que «no tots porten formalitzacions en Lean» i que «molts, però no tots, els manuscrits han estat formalitzats». Afegeix que «alguns dels resultats sense formalitzar podrien tenir problemes» i diu que s'esforçarà per arreglar-los amb rapidesa.

O sigui: la mateixa font col·loca el seu material a les tres caselles de la taula alhora. El 6 d'octubre no deia quants n'hi havia a cadascuna; el 7 va posar una part del recompte —«300 / 719 = ~42 %» dels resultats principals formalitzats— i va retirar tres manuscrits, amb la qual cosa el catàleg va quedar en 719. Donar els 722 per «verificats en Lean» els ficava tots a la primera casella, que és justament el que el repositori no afirmava: els 419 que no estan formalitzats continuen a la del mig, pendents.

L'empresa afegeix que conservarà l'historial públic i que registrarà les correccions com a versions noves, en lloc de substituir el que hi havia abans. Els tres manuscrits retirats porten ja un avís que explica el buit i un enllaç al manuscrit arxivat.

Resoldre un problema i demostrar un teorema no són el mateix

La segona confusió viatja amb la primera i té la seva pròpia data: el 12 de setembre de 2026, quan una IA va resoldre l'últim problema pendent de FrontierMath, la prova de referència de matemàtiques amb què es mesuren els models. Allò es va explicar com «resoldre», i publicar la demostració d'un teorema nou també s'explica com «resoldre»: la paraula és la mateixa i les dues coses no ho són.

En una prova de referència la resposta existeix abans que ningú no la busqui i l'encert es decideix comparant. Un teorema nou no té resposta guardada amb què comparar: l'únic revisable és el camí, i d'això se n'encarrega la comprovació de la demostració, a mà o en Lean. Aquí no es tracta d'encertar, sinó que l'argument aguanti sencer.

Cinc preguntes abans de creure's el pròxim titular

De tot això surt una llista curta, vàlida per a qualsevol anunci així. És un manuscrit o una demostració comprovada? Qui ho ha comprovat, una màquina o una persona? Està la formalització publicada al costat del text, per poder executar-la? L'ha revisat algú de fora de qui el va produir? I la que resumeix les quatre: es pot comprovar, o només creure?

Quan l'anunci porta el codi i el catàleg, les quatre primeres tenen resposta sense demanar permís a ningú. Si no els porta, la resposta a la cinquena és «creure».

L'Advisory Group on Mathematics and Artificial Intelligence (AGMAI), amb seu a l'Institute for Advanced Study de Princeton —nou matemàtics independents de qualsevol empresa d'IA i que, segons la seva pròpia declaració, no cobren per aquesta feina— ho va resumir el 6 d'octubre de 2026: «Aquesta publicació és el començament, no la culminació, del procés de comprensió humana i d'incorporació del treball al coneixement matemàtic».