OpenAI ha publicado 722 manuscritos matemáticos generados por un modelo interno que todavía no ha lanzado, acompañados de pruebas formales verificables. La magnitud de la entrega ha sacudido a una comunidad que aún no ha digerido las anteriores.
Qué ha publicado OpenAI en el repositorio openai/math
El 6 de octubre apareció en GitHub el repositorio openai/math, y en paralelo OpenAI publicó una entrada titulada "Sharing AI progress in mathematics". Dentro hay 722 manuscritos matemáticos, organizados en 372 familias de investigación, junto con resúmenes y formalizaciones de muchas de las demostraciones.
Los manuscritos los produjo un modelo de frontera interno de OpenAI. La compañía no ha puesto nombre al modelo, no ha dado precio ni ha abierto una API. Es, sobre el papel, un sistema que existe dentro del laboratorio y que de momento solo se asoma al público a través de estos resultados.
Sin nombre, sin precio y sin API. Eso explica buena parte del revuelo.
OpenAI afirma que los trabajos resuelven o avanzan de forma sustancial problemas abiertos de matemáticas y de informática teórica. Es una declaración de parte, y en matemáticas eso importa más que en casi ningún otro campo: un resultado solo cuenta cuando otra persona puede reproducir la demostración.
Qué son las pruebas en Lean y por qué importan
La parte más significativa del anuncio no son los 722 números, sino el hecho de que muchas demostraciones lleguen formalizadas en Lean. Lean es un lenguaje que permite comprobar demostraciones matemáticas con un ordenador: si la prueba se escribe de forma correcta, la máquina verifica paso a paso que no hay huecos ni saltos lógicos, sin depender de la buena fe de quien la firma.
Ese es justo el problema que ha perseguido a la IA en matemáticas. Un modelo puede escribir un argumento que suena plausible y esconder un error sutil. Con una formalización en Lean, ese tipo de fallo se detecta de forma mecánica. La contrapartida es que traducir una demostración a este lenguaje es lento y laborioso, y muchas veces el esfuerzo lo hacen personas.
La máquina no se cree nada. Comprueba cada paso.
OpenAI reconoce el reparto de tareas: dice que ayudó a preparar los manuscritos y a formalizar las pruebas, que asume la responsabilidad sobre su corrección, y que el argumento matemático en sí lo generó el sistema. Es decir, la IA produce el contenido y el equipo humano lo empaqueta y lo verifica.
Lo que está confirmado
- 722 manuscritos en 372 familias de investigación
- Muchas pruebas formalizadas en Lean
- Modelo interno aún sin lanzar
- Promedio de cómputo: unas tres horas de ChatGPT Pro
Lo que queda por verificar
- Ejecución independiente de las pruebas en Lean
- Revisión por pares de los resultados
- Si el modelo llegará a publicarse
Verificación en matemáticas: el punto débil del anuncio
Aquí está el matiz que separa el anuncio de un hito consolidado. Publicar formalizaciones en Lean no equivale a que alguien las haya ejecutado y confirmado de forma independiente. Los informes que han seguido al lanzamiento señalan que no se ha realizado esa verificación mecánica externa de todas las pruebas.
También se ha reportado que OpenAI compartió en paralelo una solución generada por IA para un problema del milenio relacionado con las ecuaciones de Navier-Stokes, acompañada de su prueba en Lean. Ese tipo de resultado, si se sostiene, sería enorme. Pero "si se sostiene" es la frase clave mientras no haya verificación ajena.
La comunidad matemática lleva meses en tensión por la avalancha de resultados generados por IA. No es escepticismo gratuito: en un campo donde un solo error invalida una demostración entera, los anuncios sin revisión independiente generan tanto expectación como dudas.
¿Basta con publicar la prueba o hace falta que alguien más la ejecute? Ahí está el debate.
Cómo lo justifica OpenAI y qué viene después
OpenAI dice que ha consultado a un grupo asesor independiente sobre matemáticas e inteligencia artificial del Institute for Advanced Study para definir cómo publicar estos resultados. De ahí salen los protocolos de revisión y citación del repositorio, y la promesa de seguir mejorando la exposición matemática en entregas futuras.
La compañía también publicó detalles sobre cómo obtuvo los resultados: diez resúmenes del razonamiento del modelo, estimaciones del cómputo gastado y estadísticas del número de problemas intentados. El dato que más ayuda a dimensionar el esfuerzo es que el resultado promedio consumió el equivalente a unas tres horas de razonamiento de ChatGPT Pro.
Tres horas de máquina por resultado. Multiplícalo por 722.
OpenAI asegura que sigue trabajando para publicar de forma responsable el modelo que produjo estos trabajos, y que financiará talleres y programas para que la comunidad entienda los grandes resultados que genera la IA. Es la parte del anuncio que mira al futuro más que al presente.
