OpenAI: diez resultados matemáticos formalizados en Lean y el papel del modelo interno

El 1 de agosto OpenAI publicó el manuscrito «Ten Advances in Mathematics and Theoretical Computer Science» y atribuyó los resultados a un modelo interno propio. A la vez se creó el repositorio de GitHub `openai/ten-proofs`, que pone a disposición las formalizaciones en Lean 4 de las diez demostraciones. Entre los resultados destacan la mejora del exponente para el empaquetamiento de esferas —la primera desde 1978—, la construcción de un grupo no sófico y un contraejemplo a la conjetura de rigidez de Connes. El repositorio es un proyecto Lean 4.32.0 basado en mathlib y publicado con licencia Apache-2.0: cualquiera puede recompilar las demostraciones con `lake exe cache get` y `lake build All`, y una carpeta ComparatorChallenges explica cómo hacer la verificación de forma independiente.

Las crónicas han vinculado estos resultados con «Astra», el nombre de la próxima familia de modelos anunciada por OpenAI ese mismo 1 de agosto; el manuscrito, sin embargo, solo habla de «un modelo interno», no publicado. Datos como el coste de unos 2.000 dólares en tokens o las 249 páginas del documento proceden de crónicas de terceros, porque la página oficial del anuncio es ahora mismo inaccesible. El artículo incluye agradecimientos a matemáticos humanos por la relectura y señala un trabajo independiente y simultáneo de Shuoxing Zhou, desarrollado en parte con la ayuda de GPT-5.6 Sol.

Según SiliconANGLE los argumentos matemáticos provienen del modelo, pero fueron investigadores humanos quienes convirtieron su salida en manuscritos publicables: cuánto pesa ese pulido no está cuantificado. El uso de Lean 4 desplaza el debate: el certificado garantiza la validez lógica de la demostración, pero no confirma de forma automática que el enunciado formalizado coincida con el problema abierto histórico, una comprobación que sigue siendo humana. Ninguno de los diez resultados ha pasado una revisión por pares formal. El precedente pesa: en octubre de 2025 el anuncio de diez problemas de Erdős «resueltos» por GPT-5 resultó infundado y Thomas Bloom, responsable de erdosproblems.com, lo calificó de grave tergiversación. Sobre los diez resultados de hoy ese mismo Bloom habla en cambio de «big news». Como observa el físico teórico Tobias J. Osborne, los 2.000 dólares citados son el coste de los tokens ganadores, no la cosecha total de los intentos, un dato sobre el que OpenAI no ha dicho nada. Todo esto se inscribe en el contexto de la «Leiden Declaration on Artificial Intelligence and Mathematics», publicada en junio de 2026 y respaldada, según the-decoder, por más de 3.000 matemáticos y por la International Mathematical Union, que reclama transparencia, protección de los derechos de los autores y responsabilidad humana sobre los resultados.

La verdadera noticia no es que una máquina haya hecho matemáticas —ocurre desde hace meses—, sino que esta vez cada resultado llega con un certificado Lean recompilable: para juzgar no hace falta fiarse de quien anuncia. Aun así, mientras la relación entre intentos fallidos y éxitos siga siendo un secreto industrial, evaluar la eficiencia de estos modelos seguirá siendo un ejercicio de fe más que de estadística.