OpenAI publica pruebas matemáticas pendientes de verificación

OpenAI publicó el 6 de octubre de 2026 una colección de resultados matemáticos producidos por un modelo interno, junto con formalizaciones de algunas pruebas en Lean y datos sobre cómo se obtuvieron. Los manuscritos quedaron abiertos al examen de otros investigadores; su publicación inicia una evaluación matemática, no la concluye.

El recuento publicado por AS el 12 de octubre sitúa el catálogo en 719 manuscritos agrupados en 372 familias y señala que cerca del 42 % de los resultados principales cuenta con una formalización en Lean. El porcentaje se refiere a resultados principales: no significa que esa proporción de manuscritos o de familias haya recibido aceptación independiente. Tampoco permite considerar resueltos todos los problemas abordados.

Por qué cambió el número de manuscritos

La diferencia entre los recuentos publicados corresponde a un cambio en la colección. La crónica de Retraction Watch registra que OpenAI publicó inicialmente 722 manuscritos el 6 de octubre y retiró tres al día siguiente por un error de signo; también recoge la respuesta de un portavoz de la empresa: «We welcome scrutiny and feedback from the mathematical community». El error invalidaba un argumento y afectaba a otros dos trabajos que dependían de él. Así se explica que una noticia sobre la publicación inicial y otra sobre el catálogo posterior den totales distintos.

La organización en familias añade otra diferencia que conviene mantener clara. Una familia puede reunir el resultado principal, argumentos complementarios, consecuencias o demostraciones alternativas; varios manuscritos pueden, por tanto, corresponder a una misma línea de resultados. Contar textos sirve para describir el tamaño de la publicación, pero no equivale a contar problemas demostrados y aceptados. Las retiradas muestran además una relación concreta entre trabajos: si falla una construcción compartida, las conclusiones que la usan necesitan volver a examinarse.

Qué publicó OpenAI además de las demostraciones

Una parte de los manuscritos matemáticos de OpenAI cuenta con formalización en Lean y otra permanece sin ese control.

El repositorio permite examinar más que las conclusiones anunciadas. Reúne manuscritos y materiales de apoyo, vincula trabajos relacionados y ofrece una biblioteca de formalizaciones en Lean asociadas a parte de las pruebas. También presenta información sobre el proceso con el que el modelo interno produjo resultados. Esos elementos permiten reconstruir qué afirmación se propone en cada caso y qué clase de comprobación la acompaña.

La existencia de materiales accesibles tiene un efecto preciso: otros matemáticos pueden leer un argumento, seguir sus dependencias y señalar una hipótesis omitida o un paso que no se justifica. En los trabajos formalizados también pueden examinar la versión expresada para Lean. Ninguna de esas posibilidades convierte automáticamente el catálogo completo en conocimiento establecido; cada afirmación conserva su propio estado de revisión.

Qué verifica Lean y qué queda fuera

Los resultados de OpenAI pasan por etapas distintas de generación, publicación, formalización y evaluación independiente.

Lean comprueba una prueba formal respecto de un enunciado formal. Al expresar una demostración en su lenguaje, las definiciones, las hipótesis y los pasos de la deducción deben quedar formulados con precisión. El sistema verifica si la conclusión se obtiene según las reglas y los supuestos utilizados. Esa comprobación puede descubrir un salto lógico que pasaría inadvertido en una exposición escrita y ofrece una garantía delimitada sobre lo que efectivamente se ha codificado.

La conexión con el problema original exige una revisión adicional. Hay que comprobar que el enunciado traducido a Lean expresa la misma pregunta que plantea el manuscrito y que conserva sus condiciones relevantes. Si la versión formal introduce una hipótesis más fuerte o demuestra una proposición más estrecha, una deducción correcta podría dejar pendiente la afirmación anunciada. También es necesario entender de qué definiciones y resultados previos depende la prueba.

En los manuscritos que aún carecen de formalización, el examen sigue siendo matemático: especialistas pueden leer el razonamiento, contrastarlo con trabajos anteriores y localizar posibles errores. Formalizar es una vía de comprobación rigurosa, pero publicar una prueba legible y obtener una verificación por ordenador son hechos diferentes. La proporción formalizada describe el avance de esa tarea técnica; por sí sola no mide la importancia ni la novedad de los resultados.

Del resultado generado a la validación matemática

El estado de cada afirmación puede resumirse en un diagrama: generado → publicado → formalizado → validado. «Generado» indica que el modelo produjo un argumento; «publicado», que el manuscrito está disponible para su examen. «Formalizado» señala que existe una expresión de la prueba en Lean susceptible de comprobación. «Validado» requiere una evaluación independiente de la corrección del resultado, de su alcance y de su relación con lo que ya se conocía.

El diagrama distingue estados, aunque la revisión humana y la formalización no tienen que ocurrir siempre en ese orden. Una demostración escrita puede recibir un examen especializado antes de traducirse a Lean. Del mismo modo, una formalización correcta deja a los matemáticos la tarea de juzgar si responde a la pregunta anunciada y qué aporta al campo. Por eso el catálogo no ofrece una cifra única de problemas definitivamente resueltos.

El siguiente cambio relevante será visible en las nuevas versiones de los trabajos y en las formalizaciones que se incorporen. Para saber cuáles de estas afirmaciones pasan a formar parte del conocimiento matemático, hará falta además la evaluación independiente de sus pruebas y de su significado.