«Verificado en Lean» no significa lo que parece

Publicar no es lo mismo que comprobar

Una demostración matemática clásica es un texto: alguien lo escribe, otros especialistas lo leen, siguen el razonamiento línea a línea y dicen si se sostiene. Funciona desde hace siglos y tiene un cuello de botella evidente, porque depende de que haya quien se siente a leerlo, y leer una demostración larga puede llevar meses.

El 6 de octubre de 2026, OpenAI publicó de golpe 722 manuscritos de matemáticas salidos de un modelo interno sin lanzar. Con ese volumen encima de la mesa, una distinción que solía quedarse entre especialistas pasa a ser lo primero: publicar un resultado y comprobarlo son dos cosas distintas.

Y conviene no juntar las etiquetas: «publicado en un repositorio», «formalizado en Lean» y «revisado por otros matemáticos» dicen tres cosas distintas, y ninguna de las tres implica las otras dos.

Lean no lee prosa: comprueba pasos

Lean es un lenguaje de ordenador pensado para escribir matemáticas. No admite prosa: cada paso se declara y tiene que derivarse de los anteriores con reglas que el programa conoce. Si todo encaja, Lean lo acepta; si un paso no se sigue del anterior, lo rechaza y dice en qué línea se rompe la cadena.

Ahí está la gracia y también el límite. Un «sí» de Lean es una garantía fuerte y muy estrecha: el argumento no tiene huecos lógicos. No dice que el resultado sea interesante, ni nuevo, ni que el enunciado demostrado sea el que importaba.

Y Lean no lee el artículo: comprueba la versión del argumento que alguien le ha escrito antes en su lenguaje. Ese trabajo previo explica casi todo lo demás.

Formalizar es traducir, y traducir cuesta

Formalizar es traducir una demostración de la prosa matemática a ese lenguaje que la máquina verifica. Es trabajo humano, lento y especializado: cada salto implícito hay que convertirlo en pasos explícitos, apoyándose en lo que la biblioteca de Lean ya tiene demostrado. Si falta una pieza de base, hay que demostrarla primero.

El ejemplo que mejor mide el coste es el último teorema de Fermat. Su formalización en Lean, fechada el 5 de septiembre de 2026, no se hizo porque el resultado fuera dudoso: estaba demostrado y aceptado desde hacía décadas. Aun así llevó años de trabajo.

De ahí sale una regla para leer titulares: que un resultado no esté formalizado casi nunca significa que nadie se lo crea, sino que formalizarlo cuesta y que todavía no le ha tocado.

Las tres situaciones, y la de en medio es la que engaña

Con eso ya se puede ordenar el asunto: un resultado publicado puede estar en tres situaciones, y esa diferencia es lo único que hay que retener.

Formalizada y aceptada es el caso cómodo. Formalizada y rechazada es el incómodo, pero claro: el programa ha encontrado el hueco y dice dónde está, así que la demostración, tal como está escrita, no vale.

La que se lee mal es la de en medio. «No formalizada» quiere decir que no está comprobada, no que esté desmentida: está pendiente de revisión, por una persona o por la máquina, y puede tener problemas o no tenerlos. Es un «todavía no», no un «no», y ahí se cuela la trampa: «no verificado» se lee como «falso».

Y de vez en cuando los tiene. El 7 de octubre de 2026, un día después de publicar su catálogo de manuscritos, OpenAI retiró tres: en uno, dice su propio historial, «un error de signo invalida» un argumento, y con él caían los otros dos, que usaban esa misma construcción. Un error de signo que echa abajo un paso es justo la clase de hueco que un comprobador mecánico no deja pasar: escrito en Lean, ese paso no compila. El historial no dice quién encontró el fallo ni si esos manuscritos llevaban formalización. Y lo que el caso no hace es mover de casilla a los demás: los cientos de manuscritos sin formalizar siguen pendientes, que es precisamente lo que significa la casilla de en medio.

Un manuscrito es un texto que todavía no avala nadie

La palabra «artículo» hace aquí mucho daño, porque en el lenguaje corriente suena a algo ya publicado y aprobado por alguien. En matemáticas, un texto puede estar en internet, legible y hasta citado, sin haber pasado por ningún filtro externo.

Publicar así no tiene nada de irregular: es el procedimiento habitual de la disciplina. Lo irregular es contar un manuscrito como si fuera un resultado comprobado. Así que la pregunta útil no es «¿está publicado?», que casi siempre lo está, sino «¿quién lo ha mirado, y con qué?».

La otra forma de comprobar sigue siendo humana y lenta

Las dos formas de comprobar no compiten, hacen cosas distintas: Lean decide si el argumento se sostiene y la revisión por pares decide si el trabajo aporta algo y está bien planteado. Un resultado puede pasar una y no la otra.

Por eso un catálogo lleno de formalizaciones no cierra el expediente, ni una revista sustituye a la máquina. Con más de setecientos textos nuevos de golpe, ninguna de las dos vías es instantánea.

El material del 6 de octubre, leído con esas tres etiquetas

Lo que OpenAI publicó el 6 de octubre de 2026 en un repositorio público reunía 722 manuscritos agrupados en 372 familias, salidos de unos 4.000 problemas planteados al modelo, con una media de tres horas de cómputo por resultado. Al lado iban una biblioteca de Lean y un catálogo que describe «las demostraciones formales disponibles, los artículos asociados y las configuraciones de verificación».

Lo que importa aquí es cómo se describe el repositorio a sí mismo. Dice que la colección «incluye resultados en distintas fases de verificación», que «no todos llevan formalizaciones en Lean» y que «muchos, pero no todos, los manuscritos han sido formalizados». Añade que «algunos de los resultados sin formalizar podrían tener problemas» y dice que se esforzará por arreglarlos con rapidez.

O sea: la propia fuente coloca su material en las tres casillas de la tabla a la vez. El 6 de octubre no decía cuántos había en cada una; el 7 puso una parte de la cuenta —«300 / 719 = ~42 %» de los resultados principales formalizados— y retiró tres manuscritos, con lo que el catálogo quedó en 719. Dar los 722 por «verificados en Lean» los metía todos en la primera casilla, que es justo lo que el repositorio no afirmaba: los 419 que no están formalizados siguen en la de en medio, pendientes.

La empresa añade que conservará el historial público y que registrará las correcciones como versiones nuevas, en vez de sustituir lo anterior. Los tres manuscritos retirados llevan ya un aviso que explica el hueco y un enlace al manuscrito archivado.

Resolver un problema y demostrar un teorema no son lo mismo

La segunda confusión viaja con la primera y tiene su propia fecha: el 12 de septiembre de 2026, cuando una IA resolvió el último problema pendiente de FrontierMath, la prueba de referencia de matemáticas con la que se mide a los modelos. Aquello se contó como «resolver», y publicar la demostración de un teorema nuevo se cuenta también como «resolver»: la palabra es la misma y las dos cosas no lo son.

En una prueba de referencia la respuesta existe antes de que nadie la busque y el acierto se decide comparando. Un teorema nuevo no tiene respuesta guardada contra la que comparar: lo único revisable es el camino, y de eso se encarga la comprobación de la demostración, a mano o en Lean. Ahí no se trata de acertar, sino de que el argumento aguante entero.

Cinco preguntas antes de creerse el próximo titular

De todo esto sale una lista corta, válida para cualquier anuncio así. ¿Es un manuscrito o una demostración comprobada? ¿Quién lo ha comprobado, una máquina o una persona? ¿Está la formalización publicada junto al texto, para poder ejecutarla? ¿Lo ha revisado alguien ajeno a quien lo produjo? Y la que resume las cuatro: ¿se puede comprobar, o solo creer?

Cuando el anuncio trae el código y el catálogo, las cuatro primeras tienen respuesta sin pedir permiso a nadie. Si no los trae, la respuesta a la quinta es «creer».

El Advisory Group on Mathematics and Artificial Intelligence (AGMAI), con sede en el Institute for Advanced Study de Princeton —nueve matemáticos independientes de cualquier empresa de IA y que, según su propia declaración, no cobran por este trabajo— lo resumió el 6 de octubre de 2026: «Esta publicación es el comienzo, no la culminación, del proceso de comprensión humana y de incorporación del trabajo al conocimiento matemático».