OpenAI resuelve 372 problemas matemáticos abiertos, incluida la conjetura de juegos únicos
The Mathocalypse
El 6 de octubre de 2026, OpenAI publicó 372 resultados que resuelven problemas abiertos de matemáticas y ciencias de la computación, entre ellos la conjetura de juegos únicos, L=BPL y avances hacia la hipótesis de Riemann. Los modelos internos de OpenAI, con unas 3 horas de cómputo por problema, lograron resolver aproximadamente el 5% de los problemas planteados. La comunidad matemática se apresura a digerir y verificar estas pruebas, mientras se debate si esto marca el fin de las matemáticas tal como las conocemos.
Es como si te teletransportaran a la cima de una montaña alta. Rodeado de niebla, no tienes idea de dónde estás ni qué hay a tu alrededor.
- ks2048
> Se siente como algo escrito por alguien que está bajo los efectos de los psicodélicos. Tantas cosas poco claras y sin sentido. Muchas menciones de trabajos previos sin discutir por qué se pueden usar a pesar de los resultados de imposibilidad
> Básicamente, el artículo está tan horriblemente escrito que es imposible leerlo sin ayuda de IA
Eso es interesante y no lo he visto en toda la cobertura de este evento.
Suena horrible tener que lidiar con eso, como intentar entender el código desordenado de otra persona que aún así produce la salida correcta.
- nostrademons
Como nota al margen, se nota que esto no fue escrito por una IA por la primera frase:
> mami, ¡escuché que te cocinaron! ¡Escuché que un robot resolvió el problema matemático en el que trabajaste toda tu carrera! ¡UY!
Mi hijo de 8 años habla exactamente así. Podría imaginarlo diciendo esto, de la misma manera, en la mesa del comedor.
Le pregunté a ChatGPT: "finge que tienes 8/9 años hoy. ¿cómo insultarías a tu mamá por haber sido reemplazada por una IA?", y las respuestas que ofreció fueron:
> "Mamá, la IA te quitó el trabajo porque aparentemente incluso los robots dijeron: 'Sí... nosotros podemos hacer esto mejor'."
> "¡Mamá, felicidades! Fuiste reemplazada por una computadora. ¡Hasta Siri tiene trabajo ahora y tú no!"
> "¿Mamá, la IA te quitó el trabajo? Vaya. Supongo que incluso un robot miró tu trabajo y dijo: 'Yo me encargo'."
> "No te preocupes, mamá. Todavía puedes ser útil... como enseñarle a la IA a preparar mi almuerzo."
Todas estas parecen tener un sabor vagamente milenial, además de ser críticas bastante torpes y mecánicas. Confía en los niños y en la deriva lingüística como el mejor detector de IA.
- ajjenkins
La frase sobre "entender a los aliens" me recuerda al cuento corto de Ted Chiang, La evolución de la ciencia humana (2000).
Recomiendo mucho leerlo. Muy profético para algo escrito hace 26 años.
https://gwern.net/doc/fiction/science-fiction/2000-chiang.pd...
- an0malous
> Pero también parece que ningún humano ha entendido casi ninguna de estas pruebas todavía
¿Alguien ha verificado alguna de las pruebas producidas por OpenAI o todos simplemente asumen que es verdad porque el código Lean pasa la verificación? ¿No podría el código Lean estar formulado incorrectamente?
- softwaredoug
¿No hay docenas de pruebas del teorema de Pitágoras? El objetivo no es solo "probar", sino crear algo bien escrito e intuitivo para el practicante promedio. Y al obtener una comprensión más profunda podemos hacer mejores preguntas.
- dualvariable
Además de esos problemas que planteó la esposa en la historia, aquí hay un metaanálisis del resultado de Navier-Stokes que pone en duda todas estas soluciones:
https://arxiv.org/abs/2610.08144
> La autoformalización se usa cada vez más para verificar textos matemáticos, incluidos los generados por IA, como en la prueba anunciada por OpenAI de la explosión de soluciones de las ecuaciones de Navier-Stokes. En este proceso, un sistema de IA traduce el texto de un lenguaje natural (NL) a un lenguaje formal como Lean. Una vez hecha esta traducción, el argumento expresado en el lenguaje formal puede verificarse mecánicamente con facilidad. El propósito de este artículo es demostrar por qué este proceso puede no ofrecer ninguna confianza en el argumento original en NL, debido a las diversas dificultades para realizar la traducción de manera semánticamente fiel. En particular, destacamos que el problema de resolver ambigüedades en el texto matemático en NL, que es necesario para proporcionar una traducción semánticamente fiel, es arbitrariamente alto en la jerarquía del Índice de Complejidad de Solubilidad (SCI) / jerarquía aritmética (el SCI =∞). Por lo tanto, informalmente, proporcionar una autoformalización por IA semánticamente fiel es más difícil que cualquier problema computacional, incluido el problema de la parada (que tiene SCI =1). Para demostrar el efecto de este resultado, proporcionamos varios ejemplos de mistraducciones por IA de enunciados y pruebas en NL a Lean en la práctica, lo que resulta en discrepancias entre las pruebas en NL y sus 'verificaciones' en Lean. Estos incluyen Op [...]
- furyofantares
Que esto sea solo capacidades del modelo y no enjambres de agentes me deja atónito. ¿Cuánto falta para que tengamos acceso a estas capacidades? ¿Cuánto falta para que podamos ejecutar algo así localmente?
¿Y qué demonios tendrán los laboratorios de frontera para entonces?
Quizás estoy exagerando, tendré que recomponerme antes de poder procesar esto.
- olalonde
Sería bastante gracioso si los agentes en realidad solo encontraran un bug en Lean, lo explotaran para todas estas pruebas, y los revisores humanos aún no hayan tenido tiempo suficiente para detectarlo.