La cifra que importa es 460.000: líneas de prueba formalmente verificable que OpenAI depositó en un repositorio público de GitHub el 1 de agosto para respaldar diez avances reivindicados en matemáticas e informática teórica. El artículo que los anuncia, fechado esa misma mañana, dice que los resultados provienen de una versión interna de Astra, 'nuestro próximo modelo mayor'. Cada uno de los diez resultados viene con un certificado Lean, una prueba formal verificable por máquina, en el repositorio github.com/openai/ten-proofs bajo licencia Apache-2.0. Comprobamos los archivos: los diez compilan con Lean 4.32 y mathlib, y ninguno contiene un 'sorry' ni un axioma a medida, las dos vías de escape habituales.

Los diez, tal como OpenAI los enuncia: nuevas cotas superiores para el empaquetamiento de esferas en alta dimensión hasta el umbral de Cohn-Elkies; cotas exponencialmente mejoradas para códigos binarios y esféricos; una construcción de grupos no sóficos; un contraejemplo que refuta la conjetura de rigidez de Connes; cotas inferiores para el permanente, incluida una cota de fórmula aritmética de orden n a la cuarta sobre log n; un teorema de repetición paralela exponencial para juegos cuánticos; dureza de aproximación de factor polinomial para el problema del vector más cercano; una respuesta precisa a la conjetura del volumen de Ehrhart; una cota inferior superexponencial para los números de Ramsey multicolor del triángulo, que resolvería el problema 183 de Erdős; y contraejemplos a las conjeturas de compacidad y degeneración, que resuelven los problemas 146 y 180 de Erdős. El marco de OpenAI es que cada problema llevaba al menos una década atascado. Ese encuadre es suyo, como la cifra de unos 2.000 dólares de cómputo a tarifas Sol de la API.

Esto es lo verificable de forma independiente hoy, y es más que nada y menos que una prueba. Verificable: el repositorio existe, los diez archivos Lean están, su contenido es el descrito, dos PDF compañeros (el artículo y las narraciones de razonamiento del modelo) se descargan, y el repositorio incluye configuraciones para verificación con un núcleo independiente. Aún no verificable: nadie fuera de OpenAI ha dicho haber reconstruido las pruebas; ningún matemático humano las ha revisado; y ningún experto confirma que los enunciados formalizados dicen lo que dicen los teoremas informales, el paso donde la formalización puede romperse en silencio. La señal más fuerte de no ratificación: erdosproblems.com, el rastreador de referencia, sigue listando el problema 183 como abierto con un premio de 250 dólares, mientras un rastreador menor ya lo marcó como resuelto el 1 de agosto. Thomas Bloom, que mantiene ese sitio, lo llamó 'gran noticia' y 'grande' para las construcciones, en mensajes citados por The Decoder; no pudimos recuperarlos directamente.

En el nombre, la precisión importa porque este es el artículo que la gente citará. El blog dice 'una versión interna de Astra, nuestro próximo modelo mayor'. La frase 'próxima gran familia de modelos' es del investigador de OpenAI Noam Brown, que añadió 'por desgracia, ningún problema del Milenio (aún)', y señaló que el modelo falló en otros grandes problemas. Todo lo demás es reportado, no confirmado: The Information, vía The Decoder, sitúa a Astra como una nueva clase junto a Sol, Terra y Luna, con la decisión GPT-6 frente a GPT-5.7 sin tomar y sin fecha de lanzamiento. La nota ética de OpenAI merece citarse entera: 'reivindicar autoría humana de una prueba generada enteramente por un sistema de IA tergiversaría tanto la contribución del sistema como la naturaleza del trabajo intelectual humano genuino', y la empresa dice asumir la responsabilidad de la corrección mientras los argumentos fueron generados por el modelo. Esa es la frase a la que sujetarlos cuando lleguen las reconstrucciones.