El 1 de agosto de 2026, OpenAI publicó una colección de 10 resultados en matemáticas y ciencias de la computación teórica generados por una versión interna de Astra, descrito como «nuestro próximo modelo principal». Los problemas seleccionados llevaban «sin avances en el resultado principal durante al menos una década, y en la mayoría de los casos mucho más tiempo». El coste total de compute: menos de $2.000 en tokens al precio de la API de GPT-5.6 Sol.
La publicación incluye: 249 páginas de argumentos, 62 páginas de notas de descubrimiento razonado, y un repositorio de certificados en Lean — el sistema de verificación matemática formal que permite a otros matemáticos comprobar cada paso de la demostración de forma automática.
Los problemas resueltos y por qué importan
Los 10 problemas abarcan campos matemáticos que raramente se mencionan juntos en un mismo anuncio — que Astra haya avanzado en todos ellos sin especialización previa en cada área es parte de lo que hace el anuncio notable:
- Empaquetamiento de esferas en alta dimensión: cuán densamente pueden empaquetarse esferas en espacios de más de 3 dimensiones. Relevante para teoría de información y códigos de corrección de errores.
- Disproof de la conjetura de rigidez de Connes: un problema en álgebras de operadores relacionado con grupos y teoría ergódica. Uno de los más técnicamente avanzados de la lista.
- Existencia de grupos no-sóficos: construcción del primer ejemplo concreto de un tipo de grupo algebraico cuya existencia era una pregunta abierta.
- Nuevas cotas para el empaquetamiento de esferas: distintas del primer problema; cotas sobre códigos binarios.
- Complejidad de circuitos aritméticos: nuevas cotas inferiores para calcular el permanente, relacionadas con uno de los problemas abiertos más importantes de la complejidad computacional.
- Problemas de Ramsey (Problema 21 de Erdős): el que más sorprendió a los matemáticos. Thomas Bloom, responsable del sitio erdosproblems.com, dijo en X que este resultado fue «el más sorprendente de toda la lista».
El «momento Deep Blue de las matemáticas»
El paralelismo con Deep Blue que hace Xataka en el titular de su cobertura es provocador pero tiene matices importantes. Cuando Deep Blue venció a Kasparov en 1997, ganó un juego específico con reglas definidas y un resultado verificable. Las matemáticas son diferentes: un resultado matemático requiere verificación por la comunidad antes de aceptarse como válido.
Lo que hace a este anuncio más sólido que la mayoría de «IA resuelve problema matemático» que vemos cada año es exactamente los certificados en Lean y la cantidad de material publicado. Normalmente estos anuncios consisten en un paper que describe el resultado; OpenAI publicó también las notas de descubrimiento paso a paso que muestran cómo Astra llegó a los resultados. Eso es lo que permite a los matemáticos impugnar no solo el resultado final sino el camino para llegar a él. Un certificado Lean es verificable automáticamente y sin ambigüedad — si el verificador de Lean acepta el certificado, la demostración es correcta. No hay interpretación subjetiva.
El matemático Bharath Ramsundar añadió cautela necesaria: «Estamos construyendo rápidamente una torre de resultados de IA ‘quizás verdaderos'» y pidió que los matemáticos humanos los revisen antes de integrarlos en el corpus establecido. Incluso con certificados Lean, la verificación de que el resultado responde la pregunta que se planteaba requiere comprensión conceptual.
Astra también fue presentado en privado por Sam Altman a policymakers en Washington DC — la primera aproximación informal a lo que Demis Hassabis propuso en julio como revisión pre-lanzamiento de modelos frontier.
Claude Sonnet 5 de Anthropic y otros modelos agentivos de 2026 compiten directamente en el espacio de razonamiento avanzado donde Astra está posicionado. GPT-5.4-Cyber muestra que la familia GPT-5 tiene especializaciones que van más allá del chat: Astra sería otra especialización, para razonamiento de largo plazo en múltiples pasos. La infraestructura de OpenAI con AMD es la que soporta el compute que hace posible tanto el entrenamiento de Astra como las decenas de miles de tokens que costaron los 10 problemas.
Mi valoración
Lo que más me convence es la especificidad de los materiales publicados. No es un paper que dice «nuestro modelo resolvió esto» — son 249 páginas de argumentos + certificados Lean verificables. Los matemáticos que quieran impugnar los resultados tienen todo el material para hacerlo.
Lo que más me preocupa es la selección. OpenAI publicó 10 éxitos. No publicó cuántos problemas Astra intentó y falló. Seleccionar 10 éxitos de 1.000 intentos tiene interpretación muy diferente que seleccionar 10 de 12. Hasta que no haya un denominador, el «momento Deep Blue de las matemáticas» sigue siendo más titular que conclusión.
Preguntas frecuentes
¿Cuándo estará disponible Astra para el público?
Astra no tiene fecha de lanzamiento pública. OpenAI lo describe como «un modelo interno» que están usando para investigación. Altman lo mostró en privado a policymakers. El ciclo habitual de OpenAI es usar los modelos internamente durante meses antes de un lanzamiento controlado a investigadores y luego público. Astra parece ser la siguiente gran versión de la familia GPT.
¿Qué es Lean y por qué es importante para verificar los resultados?
Lean es un sistema de verificación de pruebas matemáticas. Es un programa informático que comprueba cada paso de una demostración matemática formalmente, sin posibilidad de error humano. Si Lean acepta un certificado, la demostración es correcta en términos formales. Se usa en matemáticas de alta precisión donde los errores en demostraciones largas son difíciles de detectar visualmente. Los 10 resultados de Astra tienen sus certificados Lean disponibles públicamente.
¿Cómo se compara esto con los trabajos de IA en matemáticas anteriores?
Hay una diferencia importante con los logros anteriores. Sistemas como AlphaProof de DeepMind (2024) resolvieron problemas de la Olimpiada Internacional de Matemáticas — problemas con soluciones conocidas y verificación disponible. Los 10 problemas de Astra son problemas abiertos genuinos — no había respuesta conocida antes. Eso los hace cualitativamente más significativos, aunque la caveat de selección sigue aplicando.