OpenAI ha presentado Astra, su próximo modelo grande, sin enseñar el modelo. El 2 de agosto publicó un compendio de 249 páginas con soluciones a 10 problemas matemáticos que llevaban abiertos entre una y cuatro décadas, generadas por una versión interna de Astra y verificadas máquina a máquina en Lean 4.
La forma del anuncio dice tanto como el contenido. En lugar de una tabla de benchmarks, OpenAI ha soltado matemáticas que se pueden comprobar y ha dejado que la comunidad las audite.
Puntos clave
- 10 problemas resueltos, ninguno con avances desde hace al menos una década.
- Pruebas formalizadas en Lean 4, publicadas en GitHub bajo Apache 2.0, con recuento de "sorry" a cero.
- Coste del cómputo: unos 2.000 dólares en tokens a tarifas de la API de GPT-5.6.
- Astra sigue sin lanzarse: ni fecha, ni precio, ni nombre definitivo.
Qué resolvió exactamente
La lista no es de ejercicios de libro. Está la construcción explícita de un grupo no sófico, una pregunta que quedó colgando desde que Mijaíl Grómov introdujo la soficidad en 1999. Está la refutación de la conjetura de rigidez de Connes, planteada en 1980, construyendo infinitas familias de grupos no isomorfos que comparten el mismo álgebra de von Neumann. Y está la conjetura del volumen de Ehrhart, demostrada.
A eso se suman tres problemas de Erdős, entre ellos el 183 sobre números de Ramsey multicolor, más resultados en empaquetamiento de esferas en dimensión alta, códigos binarios y esféricos, complejidad de circuitos aritméticos, repetición paralela cuántica y aplicaciones a criptografía basada en retículos.
Lo que hace verificable el anuncio es Lean 4, un asistente de demostración que obliga a escribir cada paso de un argumento en formato legible por máquina. En Lean, la palabra `sorry` marca un hueco que el autor deja sin demostrar. El recuento de `sorry` en los certificados publicados por OpenAI es cero. Cualquiera puede descargar el repositorio y comprobarlo sin fiarse de nadie.
Qué es Astra técnicamente
OpenAI describe Astra como una familia de modelos diseñada para correr tareas largas coordinando varios agentes durante periodos extendidos. Es la línea de razonamiento en tiempo de inferencia que abrió Noam Brown, llevada a un horizonte de trabajo mucho más largo que el de un chat.
El detalle económico importa más de lo que parece: 2.000 dólares de tokens para resolver problemas que se llevan resistiendo veinte años. Si la cifra se sostiene, el coste marginal de atacar una pregunta abierta acaba de bajar a lo que cuesta una semana de un becario.
Y el modelo no está disponible. OpenAI no ha anunciado fecha de lanzamiento, ni precio, ni si sale como GPT-6 o como otra variante de GPT-5. Cualquier lanzamiento tiene que pasar antes la revisión federal de seguridad de IA.
Por qué esta vez cuesta más desmontarlo
Hay motivos para el escepticismo, y OpenAI se los ha ganado. En octubre de 2025, Kevin Weil, entonces vicepresidente de ciencia de la compañía, dijo que GPT-5 había resuelto 10 problemas de Erdős. Thomas Bloom, que mantiene el repositorio erdosproblems.com, lo calificó de "dramatic misrepresentation": el modelo se había limitado a reencontrar artículos publicados que Bloom no conocía. Weil borró el mensaje y Demis Hassabis, de Google DeepMind, llamó al episodio "embarrassing".
Esta vez Bloom ha dicho que sí es "big news" y sitúa el resultado por delante de lo anterior de OpenAI. Su matiz sigue en pie: ninguno de los 10 ha pasado revisión por pares. Formalizar en Lean garantiza que la demostración es correcta, no que el enunciado sea relevante ni que el crédito esté bien repartido.
Ese es exactamente el punto de fricción con la comunidad matemática. La Unión Matemática Internacional respaldó en junio la Declaración de Leiden, que acusa a las compañías de IA de usar investigación publicada sin consentimiento, saltarse la revisión por pares y erosionar la integridad de la prueba y la atribución. Fernando Borretti lo llevó más lejos y avisó de que acabaremos viviendo "in a demon-haunted world, full of marvelous devices whose operation we will not understand".
Anthropic ya estaba en esta carrera
El movimiento no llega en el vacío. En julio, Claude refutó una hipótesis matemática de 1939 y resolvió un problema abierto con el que Donald Knuth llevaba semanas atascado. La diferencia de formato es la que marca el terreno: Anthropic ha ido soltando resultados sueltos, OpenAI ha empaquetado diez y ha adjuntado los certificados.
Por qué importa
Si diriges una empresa, esto no cambia tu semana. Cambia lo que puedes pedirle a un modelo dentro de doce meses.
La señal útil no es "la IA hace matemáticas". Es que un modelo aguante una tarea de semanas coordinando agentes, y que el resultado se pueda verificar de forma automática. Ese par (horizonte largo + verificación mecánica) es justo lo que separa un chatbot de un sistema al que le puedes soltar un proceso entero de tu empresa sin revisarlo tú.
Donde se aplica primero es donde ya existe una verificación dura: cerrar contabilidad, cuadrar IVAs entre países, validar tarifas de forwarders, revisar contratos contra una plantilla. Si el resultado se puede comprobar solo, el modelo puede correr largo. Si no, sigues necesitando a alguien mirando cada paso.
Mi apuesta: en 2027 la pregunta en las empresas no será qué modelo usar, sino qué procesos tienes que puedas verificar automáticamente. Los que tengan esa lista hecha irán tres años por delante.
Relacionado
