El repositorio matemático de OpenAI: manuscritos, versiones y pruebas en Lean

La publicación matemática de OpenAI del 6 de octubre ofrece al público una colección de 722 manuscritos organizados en 372 familias de resultados. Una familia puede reunir varios artículos, mientras que una prueba formal puede abarcar un enunciado más limitado que el manuscrito que la acompaña. Seguir un artículo por el repositorio hasta la configuración de su prueba permite saber qué afirmación se ha seleccionado para verificar.

BIG CHANGE examinó el 7 de octubre el inventario completo de archivos del repositorio, su catálogo y una selección de artefactos de prueba. Se trata de un análisis de documentación y artefactos estáticos: no compilamos la biblioteca Lean, no ejecutamos un verificador de pruebas ni evaluamos las matemáticas. el anuncio de OpenAI describe una publicación en evolución y señala que habrá más formalizaciones.

El gran cambio

• Qué ha cambiado: Los investigadores ya pueden seguir cientos de manuscritos producidos por IA desde un catálogo público compartido hasta los archivos de apoyo y, para algunos resultados, hasta los enunciados formales y las implementaciones de prueba propuestas.
• Por qué importa: Un matemático que esté valorando usar un resultado puede consultar el enunciado elegido para la verificación, sus supuestos y su relación con el artículo. La organización del repositorio ayuda a identificar dónde termina un resultado formal más acotado y dónde empieza la revisión matemática adicional.
• Qué conviene seguir: OpenAI prevé añadir formalizaciones y conservar las revisiones. Estas actualizaciones importan a quienes citen este trabajo o se basen en él: una revisión debe identificar la versión y el teorema que examinó.

Contar por separado los manuscritos y las familias

Nuestro inventario encontró 722 directorios de manuscritos directamente dentro de preprints/, cada uno con un PDF, y otros 10 PDF dentro de reasoning_traces/. El mapa de manuscritos contiene 372 entradas de familias distintas y enlaces a 722 manuscritos.

Estas cifras describen objetos distintos:

El README del repositorio explica estas categorías y advierte que la verificación es desigual. Algunos resultados carecen de formalizaciones en Lean, y OpenAI señala que el trabajo no formalizado puede contener problemas. El catálogo de formalizaciones registra el alcance como «Partial progress» y el estado de revisión como unchecked. Estos campos son metadatos de publicación, no el resultado de una ejecución del verificador por parte de BIG CHANGE.

Los archivos públicos se pueden consultar sin una cuenta de OpenAI. El anuncio describe el modelo que los generó como interno y afirma que OpenAI trabaja para publicarlo. Por tanto, poder acceder a estos documentos no implica tener acceso a ese modelo.

Fijar la versión antes de seguir una prueba

La instantánea del repositorio utilizada aquí corresponde al commit adc7f1241b42e322a6451854ab7e4b4c146bf78a, fechado el 6 de octubre de 2026 a las 21:58:50 UTC. Los enlaces que incluyen ese identificador conservan la instantánea examinada; los que contienen main siguen la rama predeterminada, que cambia. El README de OpenAI promete conservar las versiones anteriores cuando aparezcan correcciones o revisiones.

Empieza por el resumen general, que agrupa las familias por disciplina matemática; después utiliza el mapa de manuscritos para llegar a un artículo concreto. Guarda el nombre de su directorio, el commit del repositorio y la cita que proporciona el artículo. La fecha de un manuscrito puede diferir de la fecha de publicación de la colección pública.

La familia 003 incluye un artículo que afirma que no hay ceros a la derecha de 7/8, una prueba alternativa para una región a la derecha de 11/12 y otro artículo distinto sobre los ceros de Landau-Siegel. El directorio del primer artículo está fechado el 30 de septiembre e incluye una cita BibTeX. Registrar el artículo concreto permite mantener la distinción entre estas afirmaciones.

Su página sobre el alcance en Lean describe qué afirmaciones cubre la formalización, identifica las exclusiones y señala que omite aplicaciones posteriores del artículo. Enlaza por separado los enunciados de verificación del resultado sobre zeta, las funciones L de Dirichlet y Hecke y una brecha uniforme para los ceros reales. La verificación de un enunciado seleccionado no representa automáticamente todos los elementos de esa página.

Seguir el enunciado seleccionado hasta su configuración

Las instrucciones de OpenAI para Comparator utilizan la familia 003 como ejemplo. Comparator es una herramienta para comparar una prueba propuesta en Lean con un reto especificado. La configuración de ejemplo en JSON selecciona un teorema: que la función zeta de Riemann no se anula cuando la parte real de su argumento supera 7/8.

La configuración apunta a un módulo de reto y a otro módulo independiente con la solución. Permite los axiomas estándar propext, Quot.sound y Classical.choice, y establece enable_nanoda en false. Nanoda es un verificador independiente que Comparator puede utilizar; esta configuración no lo habilita.

El archivo de reto contiene sorry, el marcador de Lean para una prueba sin terminar. Aquí cumple una función concreta: proporciona el enunciado que debe contrastarse. La documentación de Comparator permite usar ese marcador en el reto, pero exige una prueba correcta en la solución. Encontrar sorry en este reto no dice nada, por sí solo, sobre si la solución independiente supera la comprobación. La documentación de Comparator.

Para una comprobación local documentada, se necesitan esa configuración, sus módulos de reto y solución y sus dependencias. El repositorio fija la versión Lean 4.34.1. Su manifiesto de Lake registra las revisiones de las dependencias, incluida la de Mathlib en d13f23b723b8a846827a245b89c10fc7d3f11612.

OpenAI exige comparator, landrun y lean4export en la ruta de búsqueda de ejecutables y documenta estos comandos desde el directorio lean/:

lake update
lake exe cache get
lake env comparator ComparatorChallenges/QuasiRiemannHypothesis.json

Estas son instrucciones del editor, no comandos que hayamos ejecutado. No fijan las versiones de esas tres herramientas externas. La documentación actual de Comparator exige un entorno compatible lean4export, describe los requisitos de su entorno aislado y especifica las condiciones en que una ejecución satisfactoria demuestra coincidencia con el reto, uso permitido de axiomas y aceptación por el kernel. Un informe reproducible tendría que registrar las versiones instaladas y la salida real, además del commit del repositorio.

El README de la biblioteca Lean recomienda compilar partes pequeñas de esta gran biblioteca. También documenta límites de asignación de memoria en Linux que pueden impedir una compilación completa. No medimos el tiempo de ejecución local ni el coste de hardware de este ejemplo.

Interpretar una comprobación satisfactoria dentro del alcance declarado

La referencia de validación de Lean, consultada en la versión 4.35.0-rc3, distingue entre aceptar una prueba formal e interpretar el significado del teorema. Esa versión de la documentación es distinta de la herramienta fijada en este repositorio.

Una comprobación básica satisfactoria significa que el kernel aceptó el enunciado formal conforme a sus definiciones, importaciones y axiomas. Las dependencias aún pueden contener pruebas incompletas. Lean documenta #print axioms para mostrar los axiomas utilizados, incluido sorryAx cuando hay una prueba incompleta en la cadena de dependencias.

Las comprobaciones más rigurosas vuelven a ejecutar pruebas almacenadas o comparan una solución con un enunciado especificado por separado. También dependen del entorno de verificación y de que el significado previsto esté expresado correctamente. Por eso, un informe de verificación debe indicar el reto exacto, los axiomas permitidos y la configuración del verificador externo. Ni la aceptación del kernel ni la coincidencia con un reto demuestran que una revista haya aceptado el trabajo o que se hayan formalizado todas las afirmaciones de un manuscrito.

La cifra de cómputo describe la generación

OpenAI informa que cada resultado requirió, en promedio, un esfuerzo de cómputo equivalente a unas tres horas de razonamiento de ChatGPT Pro. Su README indica que la evaluación planteó aproximadamente 4.000 problemas y que después se agruparon y seleccionaron los resultados por su importancia. También señala excepciones al procedimiento habitual. Son cifras de generación de la empresa; no indican el precio de una comprobación en Lean para el lector ni el coste agregado en dólares. Anuncio de lanzamiento, relato sobre la generación.

Para la familia 003, este análisis identifica un enunciado concreto sobre la función zeta, la solución propuesta y los axiomas permitidos por el verificador. También confirma que el ejemplo proporcionado deja Nanoda desactivado. Solo una ejecución registrada permitirá saber si la comprobación configurada tiene éxito.

Fuentes y lecturas adicionales

• Anuncio de OpenAI del 6 de octubre confirma la fecha de lanzamiento, la situación interna del modelo, las adiciones previstas y la estimación de cómputo de la empresa. Es el relato del desarrollador sobre su propio trabajo.
• El repositorio fijado proporciona el catálogo, los archivos de los manuscritos y las configuraciones de prueba examinadas aquí. Las cifras proceden del inventario completo y del mapa de manuscritos; se leyeron algunos archivos formales sin ejecutarlos. También examinamos la fuente LaTeX del resumen general para entender su organización.
• Referencia de validación de Lean explica el significado y los límites de comprobar pruebas. Consultamos la versión 4.35.0-rc3; el proyecto de OpenAI fija Lean 4.34.1.
• Documentación de Comparator explica los archivos de reto y solución, los requisitos del entorno y las garantías condicionales. No informa de un resultado de verificación para esta colección.
• Reseña de Curtis Pyke en Kingy.ai ofrece un análisis estático independiente de la publicación. Indica expresamente que no ejecutó Lean de forma independiente; no la consideramos una reproducción de una comprobación de prueba.
• Informe anterior de BIG CHANGE sobre matemáticas e IA cubre la secuencia de mayo a septiembre. Este artículo examina la estructura de los artefactos de la nueva colección y el proceso para inspeccionarlos.