Qué publicó OpenAI y qué dice tener Astra
El 6 de octubre de 2026 OpenAI difundió un anuncio titulado "Sharing AI progress in mathematics", en el que describía la producción de un conjunto masivo de resultados matemáticos generados por un modelo interno de frontera que no está disponible al público. No se trata de un lanzamiento de producto: es una muestra de lo que ese modelo es capaz de producir cuando se le deja trabajar sobre problemas matemáticos sin restricciones de uso comercial.
Junto a ese anuncio, OpenAI publicó otro texto, "Ten advances in mathematics and theoretical computer science", donde afirmó que diez de esos avances se obtuvieron con una versión interna de Astra, el nombre que la compañía ha dado a su próximo modelo principal. Es una afirmación de la propia OpenAI sobre su propio modelo no publicado: no hay, de momento, verificación externa de que esos diez resultados concretos procedan de Astra ni de que el modelo final mantenga ese rendimiento cuando llegue al público.
La estrategia recuerda a cómo los laboratorios usan los benchmarks de programación o de razonamiento para anticipar expectativas antes de un lanzamiento: se enseña un adelanto medido en condiciones propias, sin que terceros puedan todavía reproducirlo ni auditar la metodología.
Ver los datos en tabla
| Concepto | |
|---|---|
| manuscritos matemáticos publicados | 722 |
| familias de resultados | 372 |
| problemas evaluados (aproximadamente) | 4000 |
| avances atribuidos a una versión interna de Astra | 10 |
Fuente: The Verge
El tamaño del volcado: 722 manuscritos y 372 familias de resultados
Cuatro días después, el 10 de octubre de 2026, un post de la comunidad de OpenAI tituladao "First look at mathematics manuscripts from an internal frontier model at OpenAI" detalló cifras concretas: 722 manuscritos, 372 familias de resultados y una evaluación sobre aproximadamente 4.000 problemas distintos. Son cifras que proceden de la propia OpenAI o de su entorno inmediato, no de una auditoría independiente, y así hay que leerlas.
Una "familia de resultados" agrupa demostraciones o soluciones emparentadas dentro de una misma línea de problema, de modo que 372 familias repartidas en 722 manuscritos sugiere un volumen de producción muy superior a lo que un equipo humano de investigadores podría generar en el mismo plazo. Esa es precisamente la parte que ha generado más ruido: no la calidad de cada resultado aislado, sino la escala bruta del conjunto.
Comparar el volumen con el ritmo habitual de publicación matemática ayuda a entender la reacción: revistas especializadas tardan meses en arbitrar un solo artículo con una demostración nueva. Que un sistema automatizado entregue de golpe cientos de manuscritos obliga a replantear no solo la verificación técnica, sino el propio proceso de revisión por pares tal como existe hoy.
Por qué verificar esto llevará años, no semanas
The Verge recogió que los matemáticos consultados consideran que evaluar el conjunto completo requerirá años de trabajo, debido a la heterogeneidad de los métodos de verificación empleados. Algunos resultados se presentan como pruebas en lenguaje natural, el formato tradicional en el que un matemático explica un razonamiento con palabras y símbolos; otros se han formalizado en Lean, un asistente de demostración que obliga a que cada paso lógico sea verificado automáticamente por una máquina, sin margen para la ambigüedad del lenguaje natural.
Esa mezcla de formatos es el problema de fondo: una demostración en lenguaje natural puede parecer convincente a un lector humano y aun así ocultar un salto lógico que solo se revela al intentar formalizarla paso a paso. Revisar manualmente 722 manuscritos con ese nivel de detalle, familia por familia, es un trabajo que ningún equipo reducido puede acometer en poco tiempo, de ahí la expresión "pure insanity" que recoge el titular original de The Verge para describir la magnitud del reto.
No existe tampoco un criterio único y automático para aceptar o rechazar cada manuscrito: cada área matemática tiene sus propias convenciones de rigor, y trasladar todo el conjunto a un estándar homogéneo de verificación en Lean es, en sí mismo, un proyecto de varios años.
La grieta de Navier-Stokes: cuando el lenguaje natural no cuadra con Lean
TechCrunch, en un artículo publicado el 8 de octubre de 2026 y titulado "OpenAI's math solutions aren't meeting the field's standards yet", reportó una discrepancia concreta: para un problema relacionado con las ecuaciones de Navier-Stokes —que describen el comportamiento de fluidos y son uno de los problemas abiertos más conocidos de la física matemática—, la prueba en lenguaje natural y su formalización en Lean no coincidían.
Esa discrepancia es el dato más incómodo de todo el episodio, porque apunta a una limitación estructural y no a un simple error aislado: si una demostración se sostiene en palabras pero se rompe al intentar verificarla con un sistema formal, el resultado en lenguaje natural no puede darse por válido, por muy elaborado que parezca. Es exactamente el tipo de brecha que la revisión por pares tradicional está diseñada para detectar, y que aquí ha aparecido en uno de los pocos casos donde sí hubo comparación directa entre los dos formatos.
Queda abierta la pregunta de cuántas más discrepancias de ese tipo existen entre los 722 manuscritos, dado que solo una fracción del conjunto cuenta con formalización en Lean y la mayoría permanece únicamente en lenguaje natural, sin ese control cruzado disponible.