OpenAI publica 722 manuscritos matemáticos de su modelo frontier, con formalizaciones parciales en Lean

OpenAI ha publicado en GitHub un catálogo de 722 manuscritos matemáticos organizados en 372 familias, producidos por un modelo frontier interno como parte de su desarrollo. Incluye formalizaciones en Lean de muchos resultados (no de todos), 10 resúmenes del razonamiento del modelo y la estimación de cómputo usada: de media, tres horas equivalentes de ChatGPT Pro por resultado.

Qué ha ocurrido

OpenAI anunció el 6 de octubre de 2026 la publicación de «un amplio conjunto de nuevos resultados matemáticos producidos por un modelo frontier interno». El material vive en el repositorio público github.com/openai/math —creado ese mismo día— y, según el propio README, contiene 722 manuscritos organizados en 372 familias temáticas, clasificadas por disciplina matemática, con un documento de visión general, un mapa de manuscritos y una biblioteca Lean con sus configuraciones de verificación. OpenAI aclara que muchos resultados, «pero no todos», han sido formalizados en Lean y que algunos resultados sin formalizar «podrían tener problemas», que se esforzarán por arreglar. El anuncio detalla además una capa de transparencia poco habitual: diez resúmenes abreviados del razonamiento del modelo sobre resultados concretos, estimaciones del cómputo empleado en equivalentes de ChatGPT Pro —de media, unas tres horas de «thinking» Pro por resultado— y estadísticas de problemas intentados. OpenAI afirma haberse asesorado con el Advisory Group on Mathematics and Artificial Intelligence del Institute for Advanced Study para las prácticas de publicación, y anuncia financiación de talleres y programas sobre comprensión de resultados producidos por IA, además de trabajar en «liberar responsablemente» el modelo que produjo los resultados.

Por qué importa

Es la mayor volcadura pública de investigación matemática automatizada hasta la fecha, y su interés no está solo en los resultados —que incluyen áreas de peso como la conjetura de Kaplansky en característica dos o fórmulas de vidrios de spin— sino en el protocolo: OpenAI abre los manuscritos, admite sin formalizar lo que no está verificado, publica trazas de razonamiento y cómputo empleado, y remite a un comité externo independiente para las normas de publicación. Para la comunidad matemática, la prueba es ahora colectiva: revisar y validar cientos de pruebas de un sistema que la propia empresa reconoce como imperfecto. Y la promesa de liberar el modelo —sin fecha ni términos— convierte esta publicación también en un movimiento de posicionamiento en la carrera por la credibilidad científica de los laboratorios.

Qué cambió

AntesLos resultados matemáticos de modelos frontier se conocían por titulares o papers selectivos, sin catálogo público ni trazabilidad.

AhoraOpenAI abre un repositorio con 722 manuscritos, formalizaciones Lean parciales, trazas de razonamiento y cómputo empleado, asesorado por un comité externo.

ConsecuenciaLa comunidad matemática dispone de un banco público para auditar qué prueba realmente un modelo y dónde se equivoca, y otros laboratorios quedan medidos contra este protocolo.

Qué sabemos · qué no

Confirmado

• El anuncio oficial es del 6 de octubre de 2026 y el repositorio github.com/openai/math es público desde ese día; el README propio cifra el catálogo en 722 manuscritos y 372 familias.
• OpenAI publica formalizaciones Lean parciales, un resumen y resúmenes de razonamiento de diez resultados, y estima en ~3 horas de ChatGPT Pro el cómputo medio por resultado.
• La empresa declara haber seguido las recomendaciones públicas del grupo asesor de matemáticas e IA del Institute for Advanced Study y protocolos de revisión y citas en el repositorio.
• Anuncio oficial de OpenAI el 6-10-2026 y repositorio público openai/math con 722 manuscritos en 372 familias (cifras del README oficial).
• Formalizaciones Lean de «muchos, no todos» los resultados; OpenAI advierte de que los no formalizados podrían tener problemas.
• Diez resúmenes de razonamiento del modelo y cómputo medio declarado de ~3 horas equivalentes de ChatGPT Pro por resultado.
• Asesoramiento declarado con el Advisory Group on Mathematics and AI del Institute for Advanced Study.

Todavía no

• Ninguno de los resultados ha pasado aún revisión por pares; el propio OpenAI advierte de que los manuscritos sin formalizar pueden contener errores.
• Cuáles son los resultados matemáticamente más relevantes una vez los revise la comunidad.
• Cuándo, cómo y si finalmente se liberará el modelo que produjo los resultados.
• Revisión por pares: ninguno la ha pasado todavía; la validación es el trabajo pendiente de la comunidad.
• Qué resultados concretos resistirán el escrutinio.
• Condiciones y fecha de la prometida liberación del modelo.

Para ir al grano técnico

• → repo
• → docs

Qué vigilamos ahora

Las primeras validaciones o refutaciones públicas de familias concretas por matemáticos independientes; la llegada de nuevas formalizaciones Lean al repositorio; y los detalles del programa de talleres y de la futura liberación del modelo.

Validaciones o errores detectados por matemáticos independientes en las próximas semanas y el crecimiento de las formalizaciones Lean en el repositorio.