OpenAI Astra: 10 problemas matemáticos resueltos por menos de USD 2.000

El 1 de agosto de 2026 OpenAI publicó un paper titulado Ten advances in mathematics and theoretical computer science. La cifra suena a marketing, pero el método es lo que importa: usaron una versión interna de Astra, su próximo modelo frontera, para encontrar soluciones a diez problemas abiertos de matemática y ciencias de la computación que no habían tenido progreso en su resultado principal por al menos una década. Cada una le habría costado menos de USD 2.000 en tokens a precio de GPT-5.6 Sol. Y todo el trabajo está en un repositorio público de GitHub, con las pruebas formalizadas en Lean 4.

Si te movés en el mundo de los agentes, como vimos en IA Agéntica, o usás modelos para razonar sobre código complejo, como comentamos en Claude Opus 5, esto cambia la conversación. Acá te lo desgrano: qué hizo Astra, qué críticas le hacen los matemáticos, y qué podés aprovechar hoy en tu propio workflow.

Por qué esto no es "otro paper de IA" A diferencia de la mayoría de los anuncios del rubro, OpenAI no solo publicó los resultados. Subió las formalizaciones en Lean 4 de cada prueba, junto con un PDF donde el propio modelo reconstruye el razonamiento que lo llevó a la solución. Eso significa que podés verificar la corrección línea por línea, sin tener que confiar en el comunicado de prensa.

Qué hizo exactamente Astra

El setup es concreto y vale la pena entenderlo, porque cambia mucho según cómo lo mires. Le dieron a Astra un conjunto de problemas abiertos en áreas como combinatoria, teoría de grafos, análisis armónico y complejidad computacional. Para cada problema, Astra produjo:

1. Una demostración matemática en lenguaje natural (un PDF accesible).
2. Una formalización verificable en Lean 4 (un lenguaje de pruebas interactivo muy usado en investigación). Esa formalización es la que efectivamente prueba que la demostración es correcta.
3. Un PDF de razonamiento donde el modelo intenta reconstruir, a partir de sus trazas internas, cómo llegó a la solución.

Los papers viven en el repo openai/ten-proofs. Las formalizaciones en Lean son ejecutables: cualquier investigador con Lean instalado puede compilarlas y confirmar que la prueba cierra. Eso es la diferencia clave con un paper tradicional: la verificación es mecánica, no una cuestión de fe en el referee.

El dato de costo que te tiene que hacer ruido USD 2.000 por problema a precio de GPT-5.6 Sol. Si Astra es el modelo siguiente, y los precios bajan en línea con la historia de OpenAI, en doce meses podríamos estar hablando de menos de USD 200 por el mismo trabajo. Eso ya no es "investigación asistida por IA": es 外包 automatizado de razonamiento formal.

Por qué la noticia le explotó a la comunidad matemática

La reacción de matemáticos profesionales no fue celebratoria ni apocalíptica. Fue algo más interesante. Como comenta Simon Willison en su post del 1 de agosto, Terence Tao (Medalla Fields) lleva meses hablando de lo que llama "big mathematics": un futuro donde la matemática se hace en colaboración masiva entre humanos y máquinas, donde los humanos se quedan con la parte creativa y la IA hace el grueso del trabajo técnico. Astra encaja exactamente en esa visión.

Pero también hubo un ensayo muy leído, The Dark Night of Mathematics del matemático Kirwin Hampshire, describiendo lo que él llama una "crisis espiritual profunda" frente a resultados así. Es la primera vez que muchos investigadores sienten que la herramienta puede resolver problemas que ellos no podían. No esReplacement, es algo más raro: la sensación de que la frontera de tu propio campo se está moviendo sin que participes.

Una observación que resume el momento El comentario más votado en Hacker News (robinhouston) dijo algo así como: "Lo másremarkable de todo esto es que la noticia no está en el tope de Hacker News. Ya no nos asombra que la IA haga avances significativos en matemática. Hace cinco años esto hubiera sido portada del New York Times." Esa normalización dice mucho.

Las críticas que le hacen (y son válidas)

No todo es color de rosa. Los matemáticos más serios, empezando por los que comentan en Hacker News, plantearon tres objeciones técnicas que vale la pena repetir acá, porque son las mismas que vas a escuchar cuando un modelo "resuelva" algo en tu propio trabajo.

1. Falta de transparencia experimental

El reclamo más fuerte (aabhay en HN) es que OpenAI no publicó:

• Cuántos problemas le dieron al modelo en total antes de seleccionar los diez "exitosos".
• Cuántos intentos hicieron por cada uno.
• Si tuvieron acceso a un cluster de cómputo paralelo, porque eso cambia la cuenta de USD 2.000 drásticamente.

El riesgo de p-hacking es real: si probás cien problemas, informás los diez que salieron, y no decís nada de los noventa que fallaron, la métrica de "$2.000 por problema" deja de significar lo que parece. Es el mismo problema que tuvo AlphaFold en sus primeros papers, y que cualquier benchmark de IA arrastra desde siempre.

2. Los problemas son "abiertos" pero no necesariamente "difíciles"

Ser "abierto" en matemática significa que nadie publicó la solución, no que la solución sea compleja. Varios de los diez problemas eran, según matemáticos en Twitter, variantes menores de cosas conocidas o mejoras incrementales sobre resultados previos. Eso no le quita mérito al trabajo (encontrar mejoras incrementales en problemas abiertos también es investigación legítima), pero hay que leer el paper con esa lente.

3. La verificación sigue dependiendo de humanos

Lean 4 te garantiza que la prueba compila, no que la prueba es interesante, elegante o útil para el campo. La pregunta de si el resultado aporta algo al programa de investigación sigue siendo una decisión humana. Astra no reemplaza a la comunidad matemática, automatiza la parte mecánica de formalizar.

Mi lectura honesta de las críticas Las tres objeciones son justas, y OpenAI debería publicar el setup experimental completo. Pero incluso con la información que falta, el resultado de fondo sigue siendo importante: un modelo frontera pudo producir formalizaciones correctas en Lean 4 sobre problemas abiertos, y hacerlo barato. Eso era ciencia ficción en 2024.

Qué significa para nosotros, developers

Acá viene la parte que más te debería importar si programás todos los días. No necesitás esperar a Astra público para aprovechar este cambio de paradigma. Ya hay tres vectores concretos.

Verificación formal como herramienta de code review

Si alguna vez escribiste un invariante complejo o una lógica de negocio con muchos casos borde, sabés lo difícil que es convencer a un reviewer de que está bien. Lean 4 y similares (Coq, Isabelle) sirven para probar teoremas sobre tu propio código. La barrera siempre fue que escribir pruebas en Lean es lento y requiere expertise. Un LLM competente cambia esa ecuación: vos describís el invariante en lenguaje natural, el modelo te escupe la prueba formal, y vos la revisás.

El repo de OpenAI tiene ejemplos de proofs que son directamente transferibles a problemas de programación: razonamiento sobre estructuras de datos, demostración de correctitud de algoritmos, verificación de propiedades deparsers. No es un salto grande imaginar un workflow donde cada PR importante viene con su prueba en Lean generada por IA.

Modelos locales para razonamiento formal

Si te interesa probar esto sin gastar una fortuna, el patrón ya está maduro. Con Ollama, como vimos en Ollama local, podés correr modelos open-weight razonablemente competentes en razonamiento formal. No llegan al nivel de Astra, pero para proofs pequeñas sobre lógica de negocio te ahorran horas. El truco es que necesitás un modelo con contexto largo y buena capacidad de planificación paso a paso, no el más grande necesariamente.

"Big code" como nuevo paradigma

Si la big mathematics de Tao es real, va a traer aparejada una big code: proyectos donde humanos y modelos se reparten el trabajo de manera que el humano define la arquitectura, los invariantes y los casos interesantes, y el modelo escribe el código intermedio, las pruebas y los tests. Las herramientas de hoy (Claude Code, Codex CLI, los harnesses MCP que cubrimos en MCP 2.0) son los primeros esbozos de ese workflow. Lo de Astra en matemática es un anticipo de lo que viene para nuestro trabajo.

Una predicción que me juego En 18 meses vamos a tener repositorios open source con pruebas formales en Lean 4 de las librerías más usadas de cada lenguaje, generadas por modelos. Y vamos a discutir si esas pruebas son mejores que los tests tradicionales, no si reemplazan a los humanos que las escribieron.

Lo que OpenAI todavía no te dijo

Hay tres cosas que esperaría ver en los próximos meses para tomarme todo esto en serio, más allá del paper:

1. El setup experimental completo. Cuántos problemas totales, cuántos intentos, qué hardware, qué prompt base, qué temperatura, qué configuración del harness. Sin eso, el número de USD 2.000 no significa nada.
2. La liberación de Astra o un modelo equivalente. Si el resultado depende de un modelo al que nadie puede acceder, el valor práctico es limitado. Esperaría que al menos una versión "Astra-mini" aparezca vía API en los próximos seis meses.
3. Papers de matemáticos independientes replicando el resultado. Hasta que la comunidad académica no tome estos problemas, los mejore o los refute en publicaciones peer-reviewed, son resultados patrocinados por un laboratorio con interés comercial directo. No invalida nada, pero exige más cautela.

Mientras tanto, lo que ya podés hacer es empezar a experimentar con razonamiento formal asistido por IA en tus propios proyectos. Es más accesible de lo que parece, y te obliga a escribir invariantes más claros, que es un subproducto valioso incluso si nunca usás Lean.

¿Te cambia algo en tu trabajo del lunes?

Si tu día a día es CRUD y APIs, probablemente no. Si trabajás en compiladores, sistemas distribuidos, criptografía, verificación de smart contracts o cualquier lugar donde la correctitud matemática importa, este paper es un anticipo de herramientas que van a llegar a tu IDE más temprano que tarde. La pregunta no es si la IA va a formalizar el código que escribís, sino cuánto tiempo te va a llevar adaptarte cuando lo haga.

¿Probaste Lean 4 o Coq alguna vez? ¿Te imaginás usándolo como parte del code review de tu equipo? Si tenés un caso de uso interesante, contámelo en los comentarios. Esto recién empieza.

---

Fuentes y enlaces útiles:

• Ten advances in mathematics and theoretical computer science — paper original de OpenAI
• openai/ten-proofs — repo con las formalizaciones en Lean 4
• Ten advances in mathematics — análisis de Simon Willison
• Big mathematics, IEEE Spectrum — entrevista a Terence Tao sobre el nuevo paradigma
• Hilo de Hacker News — discusión técnica, críticas de transparencia