La solución de OpenAI del enunciado con forzamiento del Problema del Milenio de la ecuación de Navier–Stokes está escrita en Lean (un lenguaje de programación que permite la verificación automática de demostraciones matemáticas). Para comprobar si dicha demostración es correcta hay que analizar sus más de 423 500 líneas de código Lean repartidas en 817 archivos, que contienen 94 719 declaraciones Lean. Cualquier mínimo error conceptual (pues sabemos que no hay errores de código) en solo una de esas líneas destruiría toda la demostración. Sabemos que las IA generativas alucinan cometiendo errores conceptuales en las demostraciones largas en Lean. Pero no sabemos si en esta demostración en concreto hay alguna alucinación oculta. También sabemos que las IA generativas alucinan cuando auditan la corrección de una demostración larga en Lean de otra IA. Por ello, no podemos confiar en que una IA actual realice dicho análisis (quizás lo podrá hacer alguna futura IA mucho más poderosa dentro de un año). Por tanto, no sabemos si dicha demostración es correcta. Solo un equipo de matemáticos humanos bien financiado puede ejecutar la ingrata tarea de validación de la demostración en Lean.
Debo enfatizar que hay que validar la demostración escrita en código Lean. No se puede validar el documento escrito por IA que explica la demostración para humanos. Yo me leí dos veces las 166 páginas de dicho documento, «Finite time blowup for Navier–Stokes,» OpenAI, 08 Sep 2026 [PDF]. Los argumentos y las ideas me parecieron convincentes, pero en varios lugares la explicación me pareció incompleta. Con toda seguridad el documento se ha escrito tras leer la demostración en Lean, pero sin haber explorado la memoria de trabajo y los mensajes intercambiados entre los diez mil agentes IA que colaboraron durante 88 horas para obtener la demostración. Por ello, hay elementos clave de la demostración en Lean que están ausentes en dicho documento. Para validar la demostración por humanos hay que validar el código Lean. Porque todo el mundo sabe que las alucinaciones en la escritura de documentos científicos son uno de los grandes problemas de las IA actuales. De hecho, los artículos escritos por las IA más poderosas carecen de la elegancia y concisión de los artículos escritos por humanos. Todos los científicos lo sabemos por experiencia propia, dado que gran parte de la literatura científica actual está escrita con IA generativa.
Por ello no es sorprendente la publicación de Alexander Bastounis, Fabian Circelli, Anders C. Hansen, «Navier-Stokes lost in translation: Why Lean verification of AI autoformalisation does not guarantee correct natural language proofs,» arXiv:2610.08144 [math.AP] (06 Oct 2026), doi: https://doi.org/10.48550/arXiv.2610.08144. En dicho artículo se encuentran diferencias entre el código Lean y el documento explicativo de OpenAI. Un ejemplo es una acotación del número m de derivadas del forzamiento normalizado, que en el código Lean requiere m+5 derivadas del forzamiento, mientras en el PDF de OpenAI se escribe que bastan m+4 derivadas ($latex \|N^{-1}F\|_{C^m}\le C_m\|F\|_{C^{m+4}}$ en el documento en PDF (nótese que un humano nunca hubiera usado $latex C_m$ como constante), mientras que $latex \|N^{-1}F\|_{C^m}\le K_m\|F\|_{C^{m+5}}$ en el código Lean). Puede que te parezca una diferencia irrelevante, pero en matemáticas puede ser capital. La razón última de esta diferencia es que el documento en PDF usa una suma de Fourier convergente con decaimiento $latex (1+|k|)^{-3}$, mientras que el código Lean trabaja con una con decaimiento $latex (1+|k_1|+|k_2|)^{-4}$.
Otro ejemplo es más sustancial, para controlar un término de flujo de presión, el documento en PDF presenta una estimación que depende de una cantidad localizada $latex B_R$, en concreto,
$latex \left|\int \pi\, w\cdot\nabla\chi_R\right| \lesssim R\Big[(B_R+1)B_R^{1/2} +R^{-3/4}B_R^{3/4}\Big]$,
mientras que el código Lean demuestra una estimación distinta, que usa otra magnitud $latex A_R$, relacionada con el gradiente localizado de $latex w$, en concreto,
$latex \left|\int \pi\, w\cdot\nabla\chi_R\right| \lesssim (B_R^{1/2}+1) \left(\frac{A_R}{R}+\frac1{R^2}\right) + R^{-7/4}B_R^{3/4}$.
No hay que ser matemático para ver que la estructura de la desigualdad es completamente diferente. Lo que está validado en Lean es la segunda expresión. ¿Por qué la IA que escribió el PDF decidió modificar esta acotación? ¿Simplificó la demostración porque se puede hacer sin afectar a su corrección? ¿Cómo es posible que las diez mil IA que trabajaron no descubriesen esta simplificación?
Como titula el preprint, todo puede ser solo un «error de traducción». La demostración en Lean puede ser correcta. Pero lo que sabemos con seguridad es que el documento en PDF de OpenAI no permite inferir si la demostración correcta. Para los expertos en IA esto no es algo nuevo; todos sabemos que este tipo de alucinaciones son habituales y, lo que es peor, son inevitables (Ziwei Xu, Sanjay Jain, Mohan Kankanhalli, «Hallucination is Inevitable: An Innate Limitation of Large Language Models,» arXiv:2401.11817 [cs.CL] (22 Jan 2024), doi: https://doi.org/10.48550/arXiv.2401.11817; Atsushi Suzuki, Yulan He, …, Zhongyuan Wang, «Hallucinations are inevitable but can be made statistically negligible,» arXiv:2502.12187 [cs.CL] (15 Feb 2025), doi: https://doi.org/10.48550/arXiv.2502.12187). Por ello, para verificar la demostración hay que recurrir a un equipo de matemáticos que explore con todo detalle el código Lean de la demostración. Sin ayuda de IA, costará muchos años. Con ayuda de IA, se puede acelerar. Pero hay que hacerlo. Y alguien tiene que financiar al equipo de investigadores que, cual quijotes, emprendan esta lucha contra los molinos que parecen gigantes.
Entonces, si lo he entendido bien, si la demostración la hubieran obtenido humanos sin IA ¿Sería más concisa e inteligible? Si fuera así ¿Sería igual de detallada que la codificada en Lean?
Jose B, si la demostración la hubieran obtenido humanos sin IA sería mucho más larga, pero también mucho más inteligible, instructiva, elegante y útil. Sería mucho más difícil de codificar en Lean y exigiría un código en Lean mucho más largo (si se hubieran ayudado con IA como Gauss) o muchísimo más largo (si lo hubieran hecho todo a mano, incluso el Lean).
francis, que piensas de lo que dice tao aquí https://teorth.github.io/tao-web/ai-views.html
Lo he ojeado por encima, pero no me parece relevante. Tao quiere liderar el progreso de la matemática, ser el adalid de la comunidad matemática, pero el impacto de la IA es tan grande y la IA evoluciona tan rápido que este tipo de opiniones en pocos meses se vuelven papel mojado. Tao cada mes dice algo diferente y se inventa nuevas historietas que contar a sus (futuros) nietos.
La alucinación es una propiedad de la IA , está forzado a darte una respuesta y está es la parte comercial y de costo. Es decir un modelo básico te dar respuestas si o si y lo hará con la primera respuesta que encuentre con las simplificaciones menos pertinentes .
Es correcto, pero los nuevos modelos de pensamiento adaptativo si están capacitados para simplemente decir, no tengo una respuesta concluyente siempre que se les instruya brevemente con la condición de que,
si no tienes respuesta concluyente debes decirlo, no inventes ni alucines respuesta sin una base solida
Si haces esto enos nuevos modelos de Claude o glm 5.3 mitigas las alucinaciones
Es obvio que utilizo el método Pseudoespectral para obtener un blow up,de otra manera ,si lo hubiese hecho como marca la norma de Fefferman,jamás lo hubiera logrado dado que aplicó una fuerza externa en todo el proceso ,es un FEO TOY MODEL ,como tantos .
Mauricio, no entiendo tu comentario. Yo uso métodos pseudoespectrales para estudiar el blow-up en ecuaciones en derivadas parciales usando análisis numérico. Pero la demostración de OpenAI no usa métodos pseudoespectrales. Tampoco incumple con “la norma de Fefferman”, OpenAI demuestra los enunciados (C) y(D) del enunciado oficial de Fefferman. La demostración formalizada en Lean (si al final se confirma que es correcta y no aprovecha alguna puerta trasera en Lean) está en perfecto acuerdo con los enunciados (C) y (D) de Fefferman. Por supuesto, no aporta nada para los enunciados (A) y (B) de Fefferman, pero esa es otra cuestión.
Efectivamente Francis.
Pero es aún peor que todo eso. Las matemáticas en su estado actual son un lenguaje semiformal (evolución histórica que ha incorporado notacion simbólica de los logicos, los algebristas etc etc).
Aunque más rigurosa que en ninguna época anterior, la realidad es que sigue siendo un sistema con bordes borrosos (hay resultados complejos que realmente terminan siendo aceptados por consenso social un punto elitista de media docena y a veces menos que entienden áreas ultraespecificas).
La unica solución de «rigor absoluto» es el de la re-escritura de las matemáticas en un lenguaje «exacto» con reglas exactas y demostraciones mecánicamente verificables.
CAMINO 1: Crear un lenguaje (nuevo) exacto que refleje de forma clara las estructuras subyacentes expresivas. Debería conseguir una teoria de conjuntos sin contradicciones, sin usar tipos y de forma natural simple, y además tener capacidades algoritmicas y autometalinguisticas «controladas»
¿Por qué? Porque esas son las capacidades del lenguaje matematico real, el que buscamos «formalizar». Y además deberíamos conseguir una formalización que desvele una «estructura gramatical subyacente» de forma casi «evidente». Un matematico humano seguirá escribiendo en semiformal y será posible una auto-formalización «casi directa».
CAMINO 2: Como nadie ha sabido encontrar el camino 1 (que es la carta a los reyes magos) hemos terminado con sistemas formales de «tipos» (un concepto ajeno a la práctica matemática semiformal) y otras particularidades. Como LEAN. Estos lenguajes no «reflejan» los conceptos y estructuras expresivas subyacentes sino que son UNA TRADUCCIÓN a otro lenguaje «ALIENÍGENA» . De hecho «formalizar a LEAN» es un laberinto. En casos complejos puede ser imposible saber si la «traduccion a LEAN» es realmente lo mismo.
La IA usando LEAN no es el futuro de las matemáticas porque LEAN es un accidente histórico «defectuoso».
Naturalmente sólo hay una forma de probar esta afirmación, y es mostrando que el camino 1 es posible (aunque en 120 años nadie ha sabido cómo).
El proyecto (https://ulogicmind.ai) está trabajando exactamente en ofrecer una solución al razonamiento en IA desde los fundamentos del nuevo lenguaje lógico subyacente ULOGIC (para tirar LEAN a la basura cuanto antes). Pero eso será otra historia.
Resumiendo: El usar LEAN para formalizar razonamientos es como el chiste ese del borracho que busca las llaves debajo de la farola porque es donde hay luz (aunque las llaves no estén ahí)
O sea que sí, la situación es como dices y aún peor (defectuosa) de lo que cuentas y parece.
Leopoldo, en matemáticas se avanza en tres fases que usan lenguajes diferentes: intuitivo, formal y riguroso. Gran parte de las matemáticas contemporáneas aún no han llegado a la fase de rigor, porque están en desarrollo (pero así ha ocurrido siempre y seguirá ocurriendo siempre). Por supuesto, Lean solo certifica el enunciado formalizado, no puede certificar la traducción a texto humano, pero no se puede calificar a Lean de “accidente defectuoso” y tampoco creo que se pueda firmar que usar Lean sea “buscar bajo la farola”. Lean es una herramienta. Si se usa bien será útil. Si no se usa bien será inútil. Lo que no quita que en mi opinión, el uso correcto de Lean debería ser inculcado en las Facultades de Ciencias Exactas desde el primer curso.
Efectivamente LEAN es una herramienta.
Es una herramienta «defectuosa» porque es posible crear un lenguaje «infinitamente mejor» por lo siguiente:
. Superar el eterno problema de las contradicciones conjuntistas SIN USAR TIPOS. Existen caminos que lo consiguen en los que ZF se convierte en una estructura más como pueda ser un grupo (ZF se vuelve innecesario).
. Disminución radical de la distancia entre expresion semiformal y la formal. La formalización se vuelve «natural» y la puede hacer cualquiera (aprendes cómo en tres minutos). LEAN es una traducción a un lenguaje muy diferente y se necesita «ser un doctor experto» para manejarlo.
. Incluir capacidades autometalinguisticas varias. Por ejemplo la notacion semiformal habitual de puntos suspensivos x1…xn es un artefacto expresivo cotidiano que es una expresion y una metaexpresion al mismo tiempo
. Incluir capacidades procedimentales en el nivel logico fundamental donde la computacion de un procedimiento es hacer un razonamiento DENTRO del sistema.
Un nuevo lenguaje con esas capacidades y con una disminución de la distancia entre lo semiformal y la estructura subyacente, sin tipos, es una «especie animal» radicalmente diferente a LEAN.
Donde además una prueba formal sea tan legible como la semiformal (inviable en LEAN).
LEAN es un intento de resolver el problema de la formalización.
Pero pronto se verá y será evidente para todos que LEAN es un camino equivocado.
Tampoco se van a morir las matemáticas por LEAN, no seamos catastrofistas. Ya saldrá otra cosa, si no nos extinguimos antes.
Al fin un camino convincente de parte de los matemáticos y no simplemente quejarse de que no es la forma de presentar pruebas o que es una comunidad de amigos que se reunen a discutir avances. Estos investigadores analizan si la traducción del lenguaje natural a Lean es exacta y encontraron que no. Me pregunto si intentaron corregir esas líneas que no coinciden con las de la prueba en inglés y ver si Lean compilaba bien o daba error. Capaz que corregir esos puntos que destacan (capaz que había más) no es tan fácil, pero creo que la IA traduce de lenguaje natural a Lean bastante rápido, es raro que no le hayan hecho auditorías de correspondencia entre estos dos lenguajes.
Quema, no, no fueron capaces de corregir dichas líneas, pues no tienen conocimientos suficientes para ello. Usaron IA para detectar los errores de traducción. Pero no tienen conocimientos para entender dichos errores con suficiente profundidad como para corregirlos (si fuese necesario). Por ello, ni afirman que la demostración en Lean esté mal, ni tampoco afirman que la demostración del PDF esté mal, solo afirman que hay diferencias entre ambas demostraciones. Nada más y nada menos, lo que la IA les ha ayudado a detectar.
Es raro que OpenAI no haya auditado la correspondencia entre el lenguaje natural y el código Lean y si lo hicieron se les escapó o exista otra explicación. Algunas diferencias son demasiados gruesas.
Quema, desde el punto de vista de OpenAI, ¿qué gana haciéndolo? Hace meses contrataba a matemáticos para hacerlo. Ahora, ¿para qué gastar el dinero de forma inútil? Por cierto, para la hipótesis cuasi-Riemann se han contratado matemáticos, que han reescrito el PDF de la demostración para facilitar su comprensión por parte de otros matemáticos (que se sepa este es el único problema de los 722 originales en el que OpenAI se ha gastado dinero en ello). En https://github.com/openai/math/tree/main/preprints/The-Quasi-Riemann-Hypothesis-October-5-2026 puedes leer «This paper was written with human assistance» (que quizás fueron matemáticos empleados de OpenAI para no gastarse ni un dólar más que su sueldo).
Hola Francis, estuve leyendo acerca del premio Nobel de física y te diré que quedé peor que antes . Cuando un neutrino ultraenergético colisiona con un nucleón dando como resultado hadrones, mesones, piones etc . En algunos sitios dicen que la energía la aporta el neutrino para crear los bosones W y Z y en otros que es el vacío cuántico . Además que cuando un nucleón cambia su identidad en forma espontánea los bosones W y Z desaparecen luego sin generar una cascada de partículas ya que el principio de indeterminación de Heisenberg para Energía y tiempo lo permite y, que en cambio cuando es por colisiones con nucleones dichos bosones sí se desintegran en partículas . Cómo ves son hartas dudas que me ha dejado tratar de entender este asunto y para que decirte lo que se inventa la IA … todas tienen versiones distintas . Un gran saludo de Uruguay.
Oganeson, los neutrinos son neutros para la carga eléctrica y para la carga de color, pero están cargados con hipercarga débil. Por ello, los neutrinos solo pueden interaccionar mediante la interacción débil, las llamadas «corrientes débiles cargadas» mediadas por bosones W virtuales y las «corrientes débiles neutras» mediada por bosones Z virtuales. Recuerda que dos electrones interaccionan entre sí intercambiando fotones virtuales (en realidad solo es una forma de hablar, pues intercambian campo electromagnético cuántico, que se describe mediante fotones virtuales en el límite perturbativo); de la misma forma, dos quarks interaccionan entre sí intercambiando gluones virtuales (es decir, campo cromodinámico cuántico). Un neutrino interacciona con un quark o con un electrón intercambiando bosones W o Z virtuales (de nuevo, campo débil cuántico). Los campos cuánticos tienen estados tipo partícula y estados tipo vacío (estos últimos se interpretan como «partículas» virtuales). Las partículas virtuales no son partículas, son excitaciones localizadas en el espacio y el tiempo del campo cuántico (por ello se dice que «aparecen y desaparecen», que solo es una forma de hablar).
La interacción de un neutrino con un núcleo es en realidad su interacción con un nucleón N (protón o neutrón), que es en realidad su interacción con un quark (de los que forman el nucleón). La energía que se intercambia procede del neutrino incidente y del quark con el que colisiona. En las interacciones mediadas por bosones W, «corrrientes débiles cargadas», como νₘᵤ + N → μ⁻ + X, el neutrino (muónico) desaparece (se desexcita el campo cuántico neutrínico) y se excita el campo de su leptón cargado (muón) asociado, que produce una cascasda hadrónica (X) y el cono de Cherenkov en IceCube. En las ineracciones mediadas por bosones Z, «corrientes débiles neutra», como νₘᵤ + N → νₘᵤ + X, el neutrino sigue siendo neutrino pero pierde parte de su energía, que pasa a la cascada hadrónica.
Recuerda, las partículas son estados cuánticos on-shell del campo, es decir, que cumplen con la ecuación de Einstein E² = (mc²)² + (pc)². Las «partículas» virtuales son estados cuánticos off-shell del campo, que no cumplen con dicha ecuación, E² ≠ (mc²)² + (pc)². Las fluctuaciones de punto cero del vacío cuántico se pueden interpretar como compuestas de «partículas» virtuales, es decir, estados cuánticos off-shell (incumplidores). Estas fluctuaciones cumplen con el principio de indeterminación de Heisenberg, por ello a veces se recurre a dicho principio para explicar la interpretación de dichas excitaciones de vacío como «partículas» virtuales. Pero no te compliques la vida, el lenguaje de «partículas virtuales» solo es aplicable en la descripción perturbativa del vacío cuántico y solo es una manera de relatar las cosas. La física siempre es más sutil y complicada que el relato divulgativo.
Hola, Francis, ¿podrías explicarme un poco cuáles son los posibles errores que pueden invalidar un código LEAN?
Es decir, partiendo de que hay un código LEAN que compila sin errores, ¿cuáles son las posibilidades para que el teorema no sea cierto?
Entiendo que una posibilidad es, obviamente, un bug en LEAN que permita demostrar algo falso, como demostraron con la conjetura de Collatz hace unos meses. Pero supongamos que LEAN no tiene bugs internos, entonces esto debería garantizar que la proposición que se ha escrito en el código debe sucederse necesariamente de los axiomas escritos en el código, ¿no? ¿O hay aún alguna forma de demostrar algo erróneo?
Entonces entiendo que el problema real (de nuevo, aparte de confirmar que no haya bugs en LEAN) es confirmar que la proposición que se ha codificado en LEAN se corresponde efectivamente con el teorema que se quiere demostrar, y confirmar que los axiomas introducidos en el código se corresponden con afirmaciones aceptadas como ciertas por cualquier matemático.
¿Tan complicado es comprobar estas cosas? Aunque la «demostración» contenga medio millón de líneas, si eliminamos todas las demostraciones y proposiciones intermedias y nos quedamos simplemente con los axiomas, las definiciones y la proposición del teorema, ¿cuán grande puede ser el código? ¿Varios cientos de líneas? ¿Miles?
En Lean tu defines una serie de conceptos y añades una serie de resultados previos y luego escribes un demostración, que se valida con el conocimiento establecido en Lean y dichas definiciones y resultados. Si para un demostración concreta, modificas un definición, Lean puede validar que el código compila sin errores, aunque la demostración sea incorrecta, porque las definiciones están mal. Este error fue cometido muchas veces por IA el año pasado cuando alucinaban mucho; ahora es más difícil, pero no imposible.
Por otro lado, todas las semanas se descubren nuevos errores en el núcleo de Lean y en las descripciones de definiciones y teoremas de ciertas áreas de la matemática. Una IA podría explotar alguno de esos errores (antes de que sea corregido) para demostrar de forma incorrecta alguna conjetura.
En cuanto al tamaño, una demostración típica de IA está partida en muchísimas piezas pequeñas que encajan como un puzle. Las demostraciones humanas suelen ser mucho más largas y discursivas. Para encontrar este tipo de errores hay que mirar todo el código (todas y cada una de las líneas, pues en cualquiera de ellas puede haber una trampa). No hay un camino fácil de validación, de ahí la dificultad.
Mil gracias Francis por tu respuesta.