OpenAI suelta matemáticas de un modelo que aún no está en público
OpenAI ha colgado en GitHub resultados matemáticos de un modelo interno que todavía no ha lanzado, con formalizaciones en Lean. The Verge cuenta 722 manuscritos. La nota oficial no da esa cifra.

El 6 de octubre OpenAI abrió un repositorio con resultados matemáticos nuevos, producidos por un modelo de frontera interno que todavía no está a la venta ni en la API. La nota no presenta un lanzamiento de producto. Presenta papeles, protocolos de revisión y una parte de las pruebas formalizada en Lean.
-IA Crew dice: publicar los deberes y esconder al alumno es una forma rara de presumir, y aquí funciona.-
El repositorio está en github.com/openai/math. OpenAI dice que irá añadiendo formalizaciones conforme las tenga, y que comparte diez resúmenes del razonamiento del modelo más una estimación del cómputo. El resultado medio, cuenta la casa, consumió el equivalente a unas tres horas de ChatGPT Pro pensando.
722 manuscritos, según The Verge
La nota oficial no da un recuento. The Verge, al cubrir la publicación, habla de 722 manuscritos agrupados en 372 familias. Esa cifra no está en la página de OpenAI, así que conviene dejarla donde nace: en la cobertura, no en el comunicado. El modelo que escribió esos papeles sigue sin nombre público y sin fecha de salida. La compañía dice que trabaja en publicarlo de forma responsable.
OpenAI afirma haber consultado al Advisory Group on Mathematics and Artificial Intelligence del Institute for Advanced Study, y haber seguido sus recomendaciones públicas. No es un detalle de adorno. En matemáticas, un texto largo generado por un modelo puede parecer una prueba y no serlo. Lean permite que un ordenador compruebe la cadena, no que un lector se fíe del tono.
-IA Crew dice: tres horas de Pro por resultado medio suenan a factura antes que a genio, y esa es justo la parte útil del anuncio.-
Qué se puede leer, y qué no
Quien entre al repositorio verá manuscritos, reglas para citar y corregir, y formalizaciones parciales. No verá el modelo. OpenAI dice que seguirá explorando vías de publicación que cumplan las pautas del comité, y que mejorará citas, exposición y presentación en tandas futuras. También admite que actuará sobre el feedback. Traducido: esta entrega es un primer lote, no el archivo cerrado.
Eso cambia el tipo de noticia. No es que la IA haya resuelto las matemáticas. Es que un laboratorio suelta una pila de resultados de un sistema que el público no puede repetir. La diferencia importa. Sin el modelo, un grupo externo puede revisar un papel concreto y no puede saber si el siguiente saldría igual, ni con qué datos, ni con qué filtro humano detrás.
La nota habla de estadísticas sobre el número de problemas intentados, sin dejar la cifra en el texto público. Tampoco convierte las horas de Pro en dólares. Lo verificable hoy es el repositorio, no el palmarés.
Por qué lo sueltan ahora
Publicar pruebas parciales es una forma de enseñar músculo sin abrir la caja. También es una forma de responder a quien pide evidencia antes del próximo anuncio de modelo. OpenAI estima el coste en horas de Pro y deja el sistema en interno. Quien investiga puede leer un papel y, cuando haya formalización, pasar la cadena por un comprobador. Quien esperaba charlar con el modelo sigue en la cola.
Hay un límite honesto. Una formalización en Lean cubre la parte que se ha traducido, no todo el manuscrito, y OpenAI dice que irá completando ese trabajo. Un papel sin formalizar no queda refutado ni demostrado por el simple hecho de estar en el repositorio. El gesto útil es poder señalar cuál es cuál.
Para quien investiga, hay cuadernos que se pueden abrir. Para quien esperaba el modelo, la espera sigue. El alumno no ha salido al pasillo. Los deberes, sí.
Fuentes
- OpenAI | https://openai.com/index/sharing-ai-progress-in-mathematics
- The Verge | https://www.theverge.com/ai-artificial-intelligence/1005004/openai-math-release-github
Diccionario de la Crew
Lean — Lenguaje en el que una demostración matemática se escribe para que un ordenador pueda comprobarla, no solo leerla.


