El 6 de octubre de 2026, OpenAI publicó un repositorio con 719 manuscritos matemáticos generados con ayuda de un modelo interno de IA. La cifra impresiona, pero también invita a hacer una pausa. Un manuscrito no es lo mismo que un teorema aceptado por la comunidad; una prueba formalizada no responde por sí sola a todas las preguntas científicas; y un gran volumen de resultados cambia tanto la capacidad de investigar como la carga de revisarlos.
La noticia importa precisamente por esa tensión. Estamos ante un experimento a una escala inusual: 719 textos agrupados en 372 familias, derivados de unos 4.000 problemas planteados al sistema. Según el repositorio oficial de OpenAI, aproximadamente el 42 % de los resultados principales ya cuenta con una formalización en Lean. A la vez, el propio historial público recoge retiradas y correcciones desde los primeros días. No es una contradicción. Es una muestra bastante nítida de cómo puede ser la ciencia cuando producir candidatos resulta más rápido que comprenderlos, verificarlos y situarlos en la literatura.
Para entender el alcance real conviene separar tres capas: lo que la IA propone, lo que un verificador formal certifica y lo que la comunidad matemática considera novedoso, relevante y bien explicado. Esa distinción también sirve fuera de las matemáticas, desde el software generado por IA hasta los informes técnicos o los análisis de datos. Ya explicamos en el blog por qué las matemáticas ayudan a comprender cómo funcionan los modelos de lenguaje; esta vez el movimiento va en sentido contrario: qué ocurre cuando esos modelos empiezan a producir matemáticas a gran escala.
Qué ha publicado OpenAI exactamente
La presentación oficial describe una colección de resultados obtenidos con un modelo de frontera interno que todavía no se ha lanzado públicamente. Los materiales están disponibles en GitHub, con versiones sucesivas y archivos de formalización cuando existen. OpenAI acompaña la colección con diez resúmenes de razonamiento pensados para facilitar el examen humano y anuncia sesiones de trabajo con matemáticos.
El repositorio aporta contexto cuantitativo útil. Se intentaron alrededor de 4.000 problemas y, de media, cada resultado consumió unas tres horas de tiempo de razonamiento de ChatGPT Pro. Esa media habla de cómputo utilizado, no de tres horas humanas ni de una medida directa de dificultad. Tampoco significa que los 719 manuscritos resuelvan 719 grandes problemas abiertos: hay familias relacionadas, distintos niveles de alcance y diferentes estados de verificación.
Este matiz es esencial. La unidad publicada es el manuscrito, no una certificación universal de corrección o importancia. La propia organización del repositorio reconoce que los trabajos se encuentran en fases diferentes. Algunos tienen su resultado principal formalizado; otros incluyen una demostración matemática convencional que aún debe ser revisada; y todos necesitan contexto bibliográfico y juicio experto para valorar su novedad.
Tip técnico: cuando evalúes una salida científica de IA, añade un campo de estado visible a cada afirmación: propuesta, comprobada computacionalmente, formalizada, revisada por especialistas o aceptada/publicada. No mezcles estas etiquetas en un único «verificado».
Qué verifica Lean y qué queda fuera
Lean es un lenguaje y asistente de demostración. Permite expresar definiciones, hipótesis, teoremas y pruebas de forma que un núcleo pequeño pueda comprobar cada paso. Cuando Lean acepta una prueba, ofrece una garantía muy fuerte: el enunciado formal se deriva de las definiciones, axiomas y resultados importados conforme a las reglas del sistema.
Eso elimina una parte importante de la ambigüedad de una demostración escrita solo en lenguaje natural. Un paso que «parece evidente» debe convertirse en una operación admitida, una definición o un lema previo. Además, el núcleo de Lean es deliberadamente pequeño, lo que reduce la base de software en la que hay que confiar. La documentación oficial sobre validación explica que la aceptación corresponde al enunciado elaborado y a la prueba construida a partir de sus dependencias.
Una garantía potente, pero delimitada
Lean comprueba la proposición que se le ha dado, no la intención que había en la cabeza de quien la formuló. Si el enunciado formal omite una condición relevante, modela un concepto distinto del anunciado en lenguaje natural o depende de una hipótesis excesivamente fuerte, la prueba puede ser válida y, aun así, no demostrar lo que el lector cree.
La verificación formal tampoco determina automáticamente si el resultado es nuevo, si ya existe con otra notación, si las citas son completas, si el teorema merece atención o si la demostración aporta una idea reutilizable. Son preguntas matemáticas, históricas y editoriales. Por eso el 42 % formalizado es una señal importante de control, pero no equivale a decir que ese 42 % ya ha completado todo el proceso científico.
Tip técnico: revisa por parejas el enunciado natural y el formal. Construye una tabla con hipótesis, cuantificadores, dominios, excepciones y conclusión. Cualquier elemento que aparezca solo en una de las dos versiones merece una explicación antes de dar la prueba por comunicada correctamente.
Tip técnico: para reproducir una formalización, fija la versión de Lean, la de mathlib y las dependencias. Conserva el archivo de bloqueo del proyecto y ejecuta la comprobación desde un entorno limpio. Que el código funcionase una vez no garantiza que sea reproducible meses después.
Las correcciones no son una nota al pie
El historial oficial del repositorio permite observar la revisión casi en tiempo real. El 7 de octubre se retiraron tres manuscritos por un error de signo que invalidaba una cancelación y afectaba a trabajos dependientes. También se revisaron catorce manuscritos para reparar pruebas, corregir enunciados u otros elementos; trece recibieron actualizaciones de citas; y se añadieron seis formalizaciones nuevas, hasta alcanzar 300 de 719 resultados principales.
Estos cambios no demuestran que todo el corpus sea poco fiable, pero sí impiden tratar la primera versión como un bloque cerrado y confirmado. También enseñan algo valioso: publicar un historial legible hace posible rastrear qué cambió y por qué. En investigación asistida por IA, la trazabilidad deja de ser un detalle de gestión y se convierte en parte de la evidencia.
Hay otro antecedente relevante. Tras el evento First Proof, OpenAI reconoció que una de las soluciones presentadas era incorrecta después de recibir comentarios de expertos. La empresa señaló además que el proceso incluía supervisión y selección humanas y que no era tan limpio como una evaluación controlada. Conviene recordarlo porque la evaluación de un sistema no puede reducirse al resultado más llamativo que haya sobrevivido a una selección previa.
Tip técnico: asigna a cada versión un identificador inmutable y registra por separado cambios de enunciado, prueba, dependencias, referencias y estado de revisión. Una corrección silenciosa impide saber qué evidencia respaldaba una conclusión en una fecha concreta.
El cuello de botella se desplaza hacia la comprensión
Si un sistema puede producir cientos de candidatos plausibles, el recurso escaso ya no es solo generar ideas. También lo son el tiempo de especialistas, la atención editorial y la capacidad de convertir una demostración correcta en conocimiento compartido. Leer 719 manuscritos con cuidado no es una tarea que se resuelva contando archivos o ejecutando un único comprobador.
El grupo asesor independiente AGMAI recomendó antes de esta publicación conservar revisiones, informar sobre modelos, instrucciones, tiempo y cómputo, formalizar todo lo posible y apoyar la comprensión humana. Tras el lanzamiento, subrayó que publicar es el comienzo, no el final, del proceso de comprensión. Es una idea incómoda pero productiva: una prueba que nadie puede explicar, conectar con resultados anteriores o reutilizar puede ser correcta y tener todavía un valor científico limitado.
OpenAI cumple parte de esas condiciones al ofrecer repositorio, historial, estimaciones de cómputo y resúmenes de razonamiento. Quedan, sin embargo, límites claros para la reproducibilidad externa: el modelo utilizado es interno y no está disponible, y el repositorio no permite reconstruir de manera completa cada trayectoria de generación. Esa observación no invalida los resultados; define qué puede y qué no puede auditar un tercero hoy.
Tip técnico: separa tres auditorías. La auditoría lógica comprueba la prueba; la bibliográfica busca precedentes y atribución; la auditoría de significado pregunta si el resultado responde al problema declarado y si aporta una idea comprensible. Ninguna sustituye a las otras.
Cómo revisar resultados de IA sin ahogarse en el volumen
1. Priorizar por riesgo e interés
No todos los manuscritos necesitan la misma profundidad inicial. Puede crearse una primera clasificación según impacto potencial, dependencia de otros resultados, ausencia de formalización, novedad declarada y dificultad para contrastar la literatura. Los trabajos de los que dependen muchas conclusiones deben revisarse antes que una variante aislada.
2. Tratar las dependencias como un grafo
El error de signo que afectó a varios textos ilustra una cuestión de ingeniería: cuando los resultados forman familias, una corrección puede propagarse. Registrar dependencias permite identificar los manuscritos que deben volver a evaluarse y evita que una conclusión retirada siga circulando fuera de contexto.
3. Buscar novedad con más de un vocabulario
Una idea puede existir con nombres, símbolos o supuestos diferentes. La búsqueda bibliográfica debe combinar palabras clave, objetos matemáticos, autores, referencias citadas y formulaciones equivalentes. Un modelo puede ayudar a ampliar términos, pero la atribución final requiere consultar las fuentes originales y, en áreas especializadas, recurrir a expertos.
4. Exigir una explicación aparte de la prueba
Una formalización muestra que una cadena lógica se sostiene. Una explicación revela por qué funciona, qué obstáculo resuelve y qué técnica podría reutilizarse. Las diez narraciones publicadas por OpenAI son un comienzo, no una cobertura equivalente a los 719 manuscritos. Para que el corpus se convierta en conocimiento, harán falta más exposiciones, discusiones y revisiones.
Tip técnico: crea una cola de revisión ponderada. Una fórmula sencilla puede combinar impacto esperado, número de dependencias, falta de verificación formal y incertidumbre bibliográfica. No pretende medir la verdad, sino dedicar primero el tiempo humano a los puntos donde un error tendría más alcance.
Tip técnico: antes de compartir un resultado, acompáñalo de una ficha mínima: versión, estado de revisión, enunciado exacto, supuestos, dependencias, pruebas automatizadas, referencias y responsable humano de la última comprobación.
Qué cambia para la investigación y para el software
En matemáticas, el experimento sugiere una división del trabajo más intensa. La IA puede explorar variaciones, proponer lemas y traducir parte del razonamiento a un lenguaje formal; las personas deciden qué merece atención, detectan desajustes semánticos, sitúan la contribución y construyen explicaciones. Es pronto para saber qué proporción de los 719 textos resistirá una revisión profunda o tendrá influencia duradera. Cualquier cifra al respecto sería una estimación, no un hecho disponible hoy.
La lección se extiende al desarrollo de software. Generar más código o documentación no reduce automáticamente el trabajo total: puede desplazarlo a pruebas, revisión, observabilidad, mantenimiento y gestión de dependencias. Los verificadores, los tests y los analizadores estáticos son valiosos porque acotan clases de error, pero tampoco confirman por sí solos que el producto resuelva la necesidad correcta, proteja los datos adecuados o resulte operable.
Por eso la pregunta madura no es «¿lo ha hecho una IA?», sino «¿qué afirmación exacta podemos sostener, con qué evidencia y bajo qué límites?». El corpus de OpenAI ofrece una oportunidad excepcional para mejorar esa disciplina. También pone a prueba la capacidad de la comunidad para revisar sin convertir el volumen en autoridad.
Fuentes
- OpenAI: Sharing new progress in mathematics, 6 de octubre de 2026.
- Repositorio oficial OpenAI Math.
- Historial de versiones y correcciones del repositorio.
- Theorem Proving in Lean 4: Introduction.
- Lean Language Reference: Validating Proofs.
- AGMAI: General recommendations for AI-generated mathematics, 29 de septiembre de 2026.
- AGMAI: respuesta a la publicación del corpus, 6 de octubre de 2026.
Deja una respuesta