✨︎ Resumen (TL;DR):
- OpenAI publicó en GitHub 722 manuscritos matemáticos generados por un modelo interno de IA que todavía no ha sido lanzado.
- El repositorio los ordena en 372 familias; el sistema recibió aproximadamente 4,000 problemas y cada resultado consumió recursos equivalentes a unas 3 horas de razonamiento de ChatGPT Pro.
- Las pruebas formalizadas en Lean permiten una revisión técnica, mientras AGMAI pide que la comunidad matemática evalúe el alcance de los resultados.
OpenAI publicó el 6 de octubre de 2026 una colección de 722 manuscritos matemáticos producidos por un modelo de IA interno que todavía no está disponible. Los documentos están en GitHub junto con materiales para examinar sus demostraciones. La colección reúne resultados con distintos estados de verificación y deja su evaluación en manos de la comunidad matemática.
El repositorio no presenta 722 problemas independientes resueltos. Organiza los documentos en 372 familias, que pueden agrupar un resultado principal, argumentos complementarios, consecuencias o pruebas alternativas. Por eso, la cifra de manuscritos no equivale por sí sola a un conteo de problemas resueltos.
Durante la evaluación, el sistema recibió aproximadamente 4,000 problemas, según el repositorio. Los resultados se agruparon y se seleccionaron por su relevancia para formar el catálogo publicado. Como esa selección no coincide uno a uno con los intentos, dividir 722 entre 4,000 no produce por sí mismo una tasa de éxito comparable.
La publicación también incluye 10 resúmenes del razonamiento del modelo. Son explicaciones abreviadas sobre resultados concretos y aportan información adicional sobre cómo se obtuvieron las propuestas matemáticas.
Qué significa la equivalencia con ChatGPT Pro
OpenAI estima que cada resultado utilizó, en promedio, recursos computacionales equivalentes a unas 3 horas de razonamiento de ChatGPT Pro. La referencia describe el cómputo empleado; no fija el precio de una demostración ni un tiempo de ejecución que cualquier suscriptor pueda reproducir.
El modelo utilizado sigue siendo interno. La equivalencia con ChatGPT Pro tampoco significa que sus suscriptores tengan acceso a esa misma capacidad. OpenAI afirma que trabaja para poner el modelo a disposición de forma responsable, pero el comunicado no da una fecha de lanzamiento.
Lean comprueba parte de las demostraciones
Lean es un lenguaje y asistente de demostraciones que permite expresar argumentos matemáticos para que una computadora los verifique. OpenAI comparte formalizaciones de muchas pruebas y prevé añadir más. El repositorio advierte que algunos resultados sin formalizar podrían contener problemas.
La documentación enlaza a Comparator, una herramienta para revisar pruebas en Lean. Bajo las condiciones descritas por sus desarrolladores, comprueba que la solución demuestre el enunciado esperado, utilice únicamente los axiomas permitidos y sea aceptada por el núcleo verificador de Lean.
Los axiomas son los supuestos de partida admitidos para construir una demostración. Ese procedimiento ofrece una comprobación técnica concreta, pero la evaluación científica requiere más: comprender el argumento, situarlo respecto de trabajos anteriores y explicar qué permite investigar después.
Las recomendaciones de AGMAI piden que las publicaciones identifiquen ideas previas, presenten sus demostraciones con claridad y señalen su estado de formalización.
AGMAI pide una evaluación hecha por matemáticos
El Grupo Asesor sobre Matemáticas e Inteligencia Artificial, AGMAI, vinculado al Institute for Advanced Study, señaló que su asesoría no constituye un juicio sobre el impacto de los resultados ni un respaldo al proceso seguido por OpenAI. El grupo trabaja con independencia de las empresas de IA y sus integrantes no reciben pago por esa labor.
En su declaración del 6 de octubre, AGMAI describió la publicación como el comienzo del proceso de comprensión humana e incorporación de los resultados al conocimiento matemático. También sostuvo que los investigadores deben formular sus propias preguntas y explorar caminos distintos de los elegidos para demostrar las capacidades de una IA.
Para ello, el grupo considera necesario un acceso equitativo a herramientas y recursos computacionales. Su declaración deja claro que comprobar una prueba en Lean no sustituye la comprensión del argumento, su relación con trabajos anteriores ni la explicación de qué permite investigar después.
OpenAI anunció que financiará talleres, conferencias y programas dedicados a comprender resultados importantes producidos por IA. Los materiales publicados permiten que esa discusión se centre en argumentos documentados, mientras el repositorio conservará las versiones anteriores cuando se registren correcciones o revisiones.
La colección queda en una etapa de evaluación abierta. Lean puede revisar la lógica de las pruebas formalizadas, pero la comunidad matemática todavía debe comprender los argumentos, relacionarlos con trabajos previos y establecer qué investigación permiten desarrollar. Los 722 manuscritos son el material de esa revisión, no una cuenta automática de problemas resueltos.
