OpenAI afirma que el modelo Astra sin publicar resolvió 10 problemas matemáticos abiertos

Why it matters

Astra gives OpenAI its clearest evidence that frontier models may generate auditable research results, opening a market for AI systems sold as discovery infrastructure.

OpenAI dijo el 1 de agosto que una versión interna de Astra, su próximo modelo importante, produjo nuevos resultados para 10 problemas de larga data en matemáticas y ciencias de la computación teóricas, una afirmación que empuja la competencia de vanguardia en IA más allá de las puntuaciones de benchmarks y hacia trabajo que puede ser inspeccionado por matemáticos de investigación.

Noam Brown (@polynoamial), un investigador de OpenAI, escribió en X que Astra representa "un avance importante para el razonamiento científico." Brown trabaja en razonamiento, aprendizaje por refuerzo, self-play y sistemas multiagente. Antes de unirse a OpenAI, trabajó en el laboratorio FAIR de Meta en CICERO, un sistema de IA construido para jugar el juego de estrategia Diplomacy, y en Carnegie Mellon University en los sistemas de póker Libratus y Pluribus.

El paquete de evidencia es más amplio que las tablas de referencia que normalmente acompañan el anuncio de un modelo de vanguardia. OpenAI publicó una colección de manuscritos de 249 páginas, guías de razonamiento y un repositorio público en GitHub de certificados Lean. Lean es un asistente de pruebas que puede verificar mecánicamente si un argumento formal se sigue de sus suposiciones declaradas.

Según el anuncio de investigación de OpenAI, Astra generó los argumentos matemáticos. Luego los humanos usaron el mismo modelo para prepararlos como manuscritos, tras lo cual Astra formalizó cada argumento en Lean. OpenAI dijo que asume la responsabilidad por la corrección del trabajo mientras acredita al sistema por generar los argumentos subyacentes.

Los 10 avances reclamados abarcan empaquetamiento de esferas de alta dimensión, códigos binarios y esféricos, grupos no sofic, la conjetura de rigidez de Connes, cotas inferiores para circuitos aritméticos, repetición paralela cuántica, el problema del vector más cercano, la conjetura del volumen de Ehrhart, números de Ramsey multicolor y dos conjeturas en teoría extremal de grafos.

Varios tienen consecuencias fuera de las matemáticas puras. El problema del vector más cercano es central para la teoría de retículos y la criptografía poscuántica. Las cotas inferiores para circuitos aritméticos conciernen límites fundamentales sobre la computación. La repetición paralela cuántica aborda cómo se comportan las probabilidades de éxito cuando se repiten juegos cuánticos, una cuestión ligada a la teoría de la complejidad cuántica.

Las afirmaciones más llamativas incluyen una construcción explícita de un grupo no sofic, lo que resolvería si todo grupo numerable puede aproximarse por permutaciones finitas, y una refutación de la conjetura de rigidez de Connes. El resultado sobre el empaquetamiento de esferas afirma la primera mejora desde 1978 al exponente general de empaquetamiento en alta dimensión.

OpenAI dijo que los tokens usados para encontrar las 10 soluciones costarían aproximadamente $2,000 a las tarifas de la API GPT-5.6 Sol. Esa cifra traduce tokens de inferencia a un precio de producto actual. No representa el costo de entrenamiento de Astra ni el trabajo humano requerido para seleccionar problemas, preparar manuscritos y verificar la salida.

El modelo en sí se mantiene interno. OpenAI identificó a Astra como su próximo modelo importante pero no dio fecha de lanzamiento, precios, términos de acceso ni una tarjeta de modelo. El anuncio funciona, por lo tanto, como una vista previa de capacidades respaldada por artefactos que especialistas externos pueden auditar, más que como un lanzamiento de modelo.

La amplitud de las afirmaciones separa la demostración de Astra de las exhibiciones matemáticas que los laboratorios de vanguardia publicaban un año antes. Esas publicaciones a menudo se centraban en problemas de olimpiada o benchmarks seleccionados con respuestas conocidas. La matemática de investigación requiere que un sistema identifique una ruta viable a través de la literatura técnica, produzca un argumento original y sobreviva a una revisión detallada.

Google DeepMind ha estado persiguiendo la misma transición. Su programa de investigación Gemini Deep Think usa un agente matemático llamado Aletheia para generar y revisar soluciones bajo la dirección de expertos, siguiendo resultados previos de nivel medalla de oro en competencias estudiantiles. El anuncio de Astra de OpenAI eleva la vara competitiva al presentar un lote de resultados originales propuestos a través de varios campos a la vez.

Los certificados Lean proporcionan un mecanismo de verificación más sólido que las pruebas en lenguaje natural por sí solas, pero no resuelven todas las preguntas en torno al lanzamiento. Los investigadores aún deben examinar si cada enunciado formal captura el problema abierto pretendido, si las suposiciones son apropiadas y cuán importante es el avance resultante dentro de su campo. Una prueba puede ser mecánicamente válida mientras que su importancia matemática aún requiere juicio experto.

OpenAI ha estado construyendo hacia esta afirmación. En mayo, el laboratorio divulgó que un modelo no publicado había generado una refutación de la conjetura de distancia unitaria de Erdos, un problema de geometría de 80 años. Astra convierte ese resultado anterior en una tesis de producto más amplia: el siguiente modelo de vanguardia se está construyendo como infraestructura de investigación, con el descubrimiento científico posicionado como una capacidad central en lugar de una demostración de especialista.