En la noche del 6 al 7 de octubre, ya de madrugada en España, OpenAI subió a GitHub 722 manuscritos de matemáticas. Los ha escrito un modelo interno que la empresa no ha publicado ni nombrado, y se agrupan en 372 «familias»: cada una reúne un resultado principal con sus variantes y consecuencias. OpenAI explica que evalúa sus modelos con problemas de investigación sin resolver y que ha publicado los resultados que alcanzaban un nivel de relevancia suficiente.
El 21 de septiembre, la empresa había dicho que su modelo había resuelto «más de cien» problemas abiertos, sin enseñar ninguno. Ahora los ha enseñado, y son más. Entre ellos hay afirmaciones que, de confirmarse, cerrarían preguntas abiertas durante décadas: sobre cómo se reparten los números primos, sobre los límites de los algoritmos de optimización o sobre por qué un imán sigue siendo un imán.
Lance Fortnow, un veterano de la teoría de la computación, escribió al día siguiente que su campo había avanzado más en 24 horas que en las tres décadas anteriores juntas. En la misma entrada añadía que nada de eso está verificado todavía.
Esa salvedad es la pregunta de este artículo: qué significa que estos resultados estén «comprobados». Esta vez una parte la puede revisar una máquina, algo que no ocurría con ningún anuncio anterior. Pero esa revisión tiene capas, y la mayoría del trabajo sigue por hacer.
Qué hay exactamente en el repositorio
Según el README del repositorio, el modelo recibió unos 4.000 problemas, y cada resultado consumió de media el cómputo equivalente a tres horas de razonamiento de ChatGPT Pro. La empresa no explica cómo eligió esos problemas, pero sí deja ver una proporción: de unos 4.000 intentos salieron 372 familias. Como señala Fortnow, el modelo resolvió menos del 10 % de lo que se le planteó.
Casi todo se obtuvo con el mismo procedimiento automático. El README reconoce dos excepciones sin detallarlas: una región de la función zeta de Riemann en la que no hay ceros y la conjetura de Hodge para cierta familia de objetos geométricos. Son, precisamente, los dos resultados más cercanos a problemas del milenio. Uno de los textos sobre la función zeta, además, fue editado por personas para hacerlo legible.
El repositorio incluye:
- los artículos en PDF con sus fuentes;
- diez resúmenes abreviados del razonamiento que siguió el modelo;
- una biblioteca de demostraciones formales en Lean, de la que hablaremos enseguida;
- y un compromiso de conservar el historial: las correcciones se publicarán como nuevas versiones, sin borrar las anteriores.
El propio README avisa: «Some of the unformalized results could have issues». Algunos de los resultados no formalizados podrían tener problemas.
El post del anuncio no destaca ningún resultado concreto. La lista de «grandes resultados» que circula estos días es una selección de la prensa y de los propios matemáticos. Hemos elegido cuatro que permiten entender la escala de lo que se afirma.
Cuatro resultados para entender lo que está en juego
Los números primos y la función zeta
Los números primos parecen repartirse sin orden, pero siguen una ley media que se demostró en 1896: hasta un número x hay aproximadamente x/ln x primos. La pregunta interesante es cuánto se aparta el recuento real de esa ley. Y la respuesta depende de dónde están los ceros de la función zeta de Riemann, los puntos en los que esa función vale cero.
La hipótesis de Riemann, formulada en 1859 y uno de los siete problemas del milenio, dice que todos esos ceros están sobre una línea concreta, la de parte real 1/2. Si es cierta, el error al contar primos es el más pequeño posible. Hasta hoy solo se sabía que no hay ceros justo en el borde, en la parte real 1, y en una franja que se estrecha a medida que se sube. Nadie había conseguido demostrar que existe una franja de anchura fija libre de ceros. Esa versión debilitada es lo que se conoce como hipótesis cuasi-Riemann.
OpenAI afirma haberla demostrado: no hay ceros con parte real mayor que 7/8. No es la hipótesis de Riemann, que exige llegar a 1/2, pero sería el primer avance de este tipo desde que se planteó. Otro manuscrito de la misma familia excluye además los llamados ceros de Siegel, una anomalía hipotética que obliga a que muchos teoremas sobre primos dependan de constantes que nadie sabe calcular. Un segundo manuscrito demuestra una región algo menor, a partir de 11/12, por otro camino. Es el texto que editaron personas.
Los límites de los algoritmos de optimización
Muchos problemas prácticos son demasiado difíciles para resolverlos de forma exacta a gran escala. Un ejemplo es dividir una red en dos grupos de forma que queden cortadas el máximo de conexiones (Max-Cut). Otro, elegir el menor número de nodos que toquen todas las conexiones (Vertex Cover). Para estos casos usamos algoritmos que dan una respuesta aproximada con una calidad garantizada. El de Max-Cut, por ejemplo, asegura al menos un 87,8 % del óptimo.
Desde 2002, la conjetura de los juegos únicos (Unique Games), de Subhash Khot, predice que no se puede hacer mejor en un tiempo razonable. Si es cierta, muchos de los algoritmos aproximados que ya usamos serían los mejores posibles, salvo que P = NP. OpenAI afirma haber demostrado la conjetura. Además, en un resultado aparte, afirma probar sin depender de ella que mejorar esas garantías para Max-Cut y Vertex Cover es NP-difícil, es decir, tan difícil como los problemas más duros de su clase.
Aquí hay una historia humana. Según Quanta Magazine, el 11 de septiembre empezaron a circular rumores de que OpenAI tenía la demostración. Dor Minzer (MIT) y dos estudiantes llevaban siete años con una variante del problema y la habían resuelto en abril. Tres días después de los rumores publicaron 95 páginas con un aviso en la primera: el texto estaba completo matemáticamente, pero no tenía la forma en que querían compartirlo. «There is a lot of value in failing and knowing why you failed», dijo Minzer a la revista: fallar y entender por qué tiene mucho valor.
Por qué un imán sigue siendo un imán
En un imán, los pequeños momentos magnéticos de los átomos, los espines, se alinean. La física cuántica describe ese comportamiento con el modelo de Heisenberg, y cualquier físico da por hecho que en tres dimensiones, a baja temperatura, el material conserva su magnetización. Demostrarlo con rigor era otra cosa. La versión clásica del modelo y el caso cuántico antiferromagnético, en el que los espines vecinos apuntan en sentidos opuestos, se resolvieron hace décadas. Pero la técnica que funcionó en esos casos no sirve para el imán cuántico corriente, y Elliott Lieb lo incluyó en 1999 como «Problem A» de una lista de problemas abiertos de física matemática.
OpenAI afirma haberlo demostrado para todas las dimensiones a partir de tres. Es un buen ejemplo de un tipo de resultado que suele pasar desapercibido: no cambia lo que creemos sobre el mundo, pero convierte una certeza física en un teorema.
Una pregunta clásica con una respuesta inesperada
A partir de un «grupo libre», el conjunto de todas las palabras que se pueden escribir con dos letras y sus inversas, o con tres, se construye un objeto del análisis llamado factor de von Neumann. Estos objetos aparecen en los trabajos fundacionales de Murray y von Neumann, y la pregunta, que se atribuye a Richard Kadison, es si el objeto recuerda con cuántas letras se empezó. Se considera el problema abierto más conocido de su área, y buena parte de la investigación se orientó a demostrar que los objetos eran distintos.
OpenAI afirma lo contrario: con dos letras o con tres se obtiene el mismo objeto. Si se confirma, sería uno de esos resultados que obligan a revisar la intuición de un campo entero. Además, ilustra bien el problema del que trata la siguiente sección.
El resto del catálogo
Estos cuatro son una muestra. La tabla recoge otros resultados de primer nivel y si tienen demostración formal en Lean:
| Resultado | Qué se afirma | ¿Formalizado en Lean? |
|---|---|---|
| Conjetura de Hodge para variedades abelianas CM | Un caso amplio de otro problema del milenio, planteado en 1950 | No. Además, es una de las dos excepciones al procedimiento |
| Kakeya en cuatro dimensiones | Un conjunto que contiene un segmento en cada dirección no puede ser más «delgado» que el propio espacio. El caso de tres dimensiones se resolvió en 2025 | No |
| Conjetura de Erdős sobre progresiones | Si la suma de los inversos de un conjunto de enteros es infinita, el conjunto contiene progresiones aritméticas tan largas como se quiera | Solo la parte cualitativa |
| El exponente de irracionalidad de π | π no se deja aproximar por fracciones mejor que un número cualquiera. Las mejores cotas anteriores rondaban 7,1; la nueva es 2, el mínimo posible | Sí |
| Décimo problema de Hilbert sobre los racionales | No existe un algoritmo que decida si una ecuación polinómica tiene soluciones fraccionarias | No |
| Conjeturas de Mahler | Qué cuerpo convexo, junto con su dual, ocupa el menor volumen posible, en cualquier dimensión | Sí |
Fuente: catálogo del repositorio y catálogo de formalizaciones, consultados el 7 de octubre de 2026. Descripciones simplificadas por Codin.
«Comprobado» puede significar tres cosas distintas
La novedad de esta publicación frente a las anteriores es Lean. Lean es un lenguaje en el que se escribe una demostración con tanto detalle que un programa puede revisarla paso a paso, sin fiarse de nadie. Se apoya en Mathlib, una biblioteca comunitaria de definiciones y teoremas ya comprobados. Que una demostración «compile» en Lean significa que cada paso se sigue de los anteriores.
Pero cuando se dice que un resultado está comprobado conviene distinguir tres preguntas.
Primera: ¿la demostración formal es correcta?
Esto es lo que resuelve Lean, y se puede repetir fuera de OpenAI. El repositorio incluye retos para Comparator, una herramienta que acepta una demostración solo si prueba exactamente el enunciado de referencia y usa únicamente los axiomas estándar. A las pocas horas de la publicación, varias personas ajenas a OpenAI volvieron a compilar la demostración de la región 7/8 en sus máquinas, con resultado correcto.
El repositorio contiene más de 120.000 ficheros de Lean, pero esa biblioteca cubre una parte pequeña del catálogo: 162 de los 722 manuscritos tienen su resultado principal formalizado.
Segunda: ¿el enunciado formal dice lo que creemos?
Lean garantiza que la demostración prueba el enunciado que se le ha dado. No garantiza que ese enunciado signifique lo que dice el artículo. Esta es la capa que más depende de las personas, y su dificultad varía mucho de un resultado a otro.
En el mejor caso, el enunciado es tan corto que cualquiera con algo de formación puede leerlo:
theorem riemannZeta_ne_zero_of_seven_eighths_lt_re
{s : ℂ} (hs : (7 / 8 : ℝ) < s.re) : riemannZeta s ≠ 0 := by
sorrySe lee así: para cualquier número complejo s cuya parte real sea mayor que 7/8, la función zeta no vale cero. riemannZeta es la definición de Mathlib, escrita y revisada por la comunidad antes de este anuncio. El sorry marca el hueco que debe rellenar la demostración de OpenAI, que está en otra parte de su biblioteca.
Fuente: QuasiRiemannHypothesis.lean, en el repositorio de OpenAI.
Si la definición es la de la comunidad y el enunciado cabe en dos líneas, la confianza que da Lean es muy alta. Por eso la región sin ceros de 7/8 es, hoy, el resultado mejor comprobado del catálogo.
El caso de los factores de grupos libres es distinto. Mathlib todavía no tiene esos objetos, así que el reto de Comparator los define desde cero, con definiciones escritas también por OpenAI. Con Unique Games ocurre algo parecido: el enunciado se apoya en miles de caracteres de codificaciones propias. Una demostración perfecta de una definición ligeramente equivocada demuestra otra cosa. Alguien con conocimientos del área tiene que leer esas definiciones y confirmar que capturan el problema real.
El catálogo de formalizaciones lo deja claro en dos campos: las demostraciones en Lean las escribió también un agente de IA (automation: agent), y su revisión figura como pendiente (review: unchecked).
Tercera: ¿qué hemos entendido?
Incluso con el enunciado bien formalizado, Lean suele cubrir solo el teorema principal. En la hipótesis cuasi-Riemann, la propia documentación avisa de que las aplicaciones del artículo no están incluidas. Esas aplicaciones son, precisamente, lo que interesa a un especialista en números primos.
Los otros 560 manuscritos dependen hoy de su texto en lenguaje natural y del criterio interno de OpenAI. Entre ellos está la conjetura de Hodge, uno de los dos resultados que no siguieron el procedimiento automático y que no tiene formalización.
Y luego queda lo que ningún programa revisa: qué idea hace funcionar cada demostración, si abre caminos nuevos y qué cambia en el área. Ya hablamos de este desplazamiento en cuando demostrar deja de ser el cuello de botella. Esta publicación lo hace tangible: la máquina ha puesto mucho más fácil la primera capa, y el trabajo humano se concentra en las otras dos.
Lo que pidieron los matemáticos y lo que ha llegado
El 21 de septiembre, OpenAI presentó un grupo asesor independiente de nueve matemáticos, AGMAI, con sede en el Institute for Advanced Study de Princeton. El 29 de septiembre, una semana antes de la publicación, el grupo publicó sus recomendaciones, basadas en más de 600 respuestas de la comunidad. Empezaban con una petición: que los laboratorios dejaran de probar problemas matemáticos avanzados con modelos propietarios. Esta es la comparación entre lo que pedían y lo que ha llegado:
| Lo que pidió AGMAI | Lo que ha publicado OpenAI |
|---|---|
| Formalizar en Lean con retos de Comparator | Sí, para 162 de los 722 manuscritos |
| Resumir el razonamiento de cada resultado | Diez resúmenes, no uno por resultado |
| Contar los intentos fallidos y cómo se eligieron los problemas | Unos 4.000 problemas planteados, sin desglose ni criterio de selección |
| Financiar el trabajo de entender los resultados | Compromiso de financiar talleres y congresos, sin cifras |
| Publicar en un repositorio no controlado por un laboratorio | No: en la cuenta de GitHub de OpenAI, que dice estar explorando alternativas |
| Nombre del modelo, prompts, tiempo y coste de cada resultado | No: solo el coste medio |
| Acceso amplio a los modelos | No: el modelo es interno. OpenAI dice que trabaja para lanzarlo, sin fecha |
Fuentes: recomendaciones de AGMAI del 29 de septiembre, anuncio de OpenAI y README del repositorio. Comparación elaborada por Codin.
Sin el modelo ni los prompts, nadie puede reproducir cómo se llegó a cada resultado. Eso no impide comprobar una demostración, que se sostiene o no por sí misma. Pero sí impide saber cuánto pesó la elección de los problemas, qué se intentó sin éxito o si las dos excepciones recibieron una ayuda que el resto no tuvo.
El mismo 6 de octubre, AGMAI publicó una declaración que conviene leer entera. Dice que su papel asesor no debe interpretarse como una valoración del impacto de estos resultados ni como un aval del proceso. Añade que corresponde a la comunidad juzgar hasta qué punto se han seguido sus recomendaciones. Y lo resume así: «This release is the beginning, not the completion, of the process». La publicación es el principio del proceso de entender e incorporar estos resultados, no su final.
Cómo lo ha recibido la comunidad en las primeras horas
A 7 de octubre, ningún especialista había publicado una revisión de un resultado concreto, ni se había confirmado ningún error. Lo que hay son posiciones sobre cómo leer el anuncio.
Andrew Sutherland (MIT) pidió en Scientific American tratar como no verificado lo que no pueda reproducirse: «We should ask for receipts». Daniel Litt (Universidad de Toronto) respondió en el mismo artículo con el argumento contrario. Si queremos conocer las respuestas, no tiene sentido pedir a la empresa que las guarde en secreto, y cree que será bueno para las matemáticas. Mark Braverman (Princeton) dijo a Quanta que publicar matemáticas a golpe de nota de prensa no es sano para la disciplina: «Math by press release is not that healthy for math». Aun así, reconoció que una demostración así puede abrir líneas nuevas.
Mientras tanto, la verificación ha empezado a organizarse fuera de OpenAI. Además de las recompilaciones de Lean, un catálogo comunitario de problemas abiertos ha importado cientos de resultados con la misma advertencia en cada uno: ningún matemático independiente lo ha revisado todavía. Ya marca varios como discutidos, por posibles conflictos con resultados publicados antes.
El tono de fondo tiene dos caras. Hay asombro por la escala, y lo hay incluso entre los críticos. Y hay cansancio: tras la polémica sobre la autoría de Navier–Stokes y la carta de los medallistas Fields, la crítica ya no se dirige solo a lo que dicen estos sistemas. También se dirige a quién decide el ritmo y cómo se publica.
Un test en verde solo demuestra lo que el test pregunta
El 29 de septiembre defendimos que quien anuncia cien avances debería acompañar cada uno de información suficiente para comprobarlo y construir sobre él. Esta publicación da bastante más que la anterior. Hay manuscritos completos, una biblioteca formal que cualquiera puede ejecutar e historial de versiones. Sería injusto no reconocerlo. Pero sigue faltando lo que permitiría reproducir el proceso, y sigue sin estar claro quién paga el trabajo de revisarlo.
En software conocemos bien la distinción que este caso hace visible. Que los tests pasen no demuestra que el programa haga lo correcto: demuestra que hace lo que los tests comprueban. Si la especificación está mal escrita, el código puede cumplirla a la perfección y aun así no servir. Lean ha convertido la corrección de una demostración en algo parecido a un test automático, rápido y fiable. La pregunta se ha desplazado a la especificación: si el enunciado formal es el problema que nos importa, y qué nos enseña la demostración además de que es cierta.
Por eso, la cifra que conviene seguir en los próximos meses no es 722. Hay otras tres que dirán más:
- Cuántos enunciados formales revisa alguien del área, empezando por los que se apoyan en definiciones propias.
- Cuántos resultados de primer nivel reciben una revisión de especialistas, sobre todo los que no tienen Lean, como Hodge.
- Cuántas correcciones registra el historial de versiones. Un repositorio de esta escala sin erratas sería más sospechoso que uno con ellas.
Si esas cifras crecen, esta publicación habrá servido para que la comunidad incorpore resultados reales. Si no crecen, tendremos cientos de teoremas de los que solo sabremos que una máquina dice que son ciertos.
Fuentes
- OpenAI: «Sharing AI progress in mathematics», 6 de octubre de 2026.
- Repositorio openai/math: README, catálogo de manuscritos, catálogo de formalizaciones, alcance de la formalización de la hipótesis cuasi-Riemann y reto de Comparator. Commit
adc7f124, consultado el 7 de octubre de 2026. - AGMAI: recomendaciones del 29 de septiembre de 2026 y declaración del 6 de octubre.
- Lance Fortnow: «Open No More», 7 de octubre de 2026.
- Quanta Magazine: carrera por la conjetura de los juegos únicos, 7 de octubre de 2026.
- Scientific American: reacciones de Sutherland y Litt, 6 de octubre de 2026.
- Elliott Lieb: «Problem A», lista de problemas abiertos de física matemática, 1999.
- Recompilaciones independientes de la región 7/8: Zhang-Liao/quasi-riemann y davegoldblatt/openai-zeta-proof-check. Comprueban la demostración formal, no el artículo.
- Catálogo comunitario vibemathed: importación de los resultados de OpenAI.
Nota editorial: no hemos auditado ninguno de los resultados. Las descripciones matemáticas están simplificadas para un lector no especialista y reflejan lo que afirma OpenAI, no un consenso de la comunidad.
