AICONTROLLED/LAB

JOURNAL / 2026.08.03

OpenAI atribuye a Astra diez avances matemáticos con certificados en Lean

Una versión interna del próximo modelo de OpenAI generó resultados sobre diez problemas y los formalizó en Lean; la cadena pública eleva la evidencia, pero aún no mide la tasa de éxito ni sustituye la revisión matemática.

  • Modelos
  • Matemáticas
  • Investigación
  • Datos y evaluación

OpenAI publicó el 1 de agosto una afirmación de capacidad poco habitual: una versión interna de Astra, su próxima gran familia de modelos, produjo resultados nuevos sobre diez problemas de matemáticas y computación teórica. No todos son «diez problemas resueltos» en el mismo sentido. La colección incluye soluciones a conjeturas, como la existencia de grupos no sóficos y la cota de volumen de Ehrhart, pero también avances parciales sustanciales, como una mejor cota asintótica para el empaquetamiento de esferas y nuevas cotas para códigos y para la complejidad del permanente.

La amplitud importa. Los trabajos abarcan geometría de alta dimensión, teoría de grupos, álgebras de operadores, complejidad cuántica, retículas y combinatoria extrema. La colección técnica de 249 páginas contiene enunciados y demostraciones completos, no una tabla de benchmarks. Y Astra no se limitó a redactar argumentos informales: OpenAI publicó un repositorio con formalizaciones en Lean para los resultados principales.

Ese paquete convierte el anuncio en una noticia materialmente distinta de «un modelo parece bueno en matemáticas». También obliga a separar cuatro capas de evidencia que suelen confundirse.

Cadena de evidencia desde los argumentos de Astra hasta la revisión matemática independiente

Lo que la comprobación formal añade

Según OpenAI, Astra generó los argumentos matemáticos; personas prepararon los manuscritos con ayuda del mismo modelo; después, el modelo tradujo cada argumento a un certificado en Lean. La empresa no reclama autoría humana de las ideas y asume públicamente la responsabilidad por la corrección de los trabajos.

Lean obliga a expresar definiciones, supuestos y pasos lógicos en un lenguaje que un núcleo pequeño puede comprobar. El repositorio declara que las formalizaciones principales no contienen sorry —el marcador de una demostración pendiente— y limita sus axiomas a tres extensiones estándar de la biblioteca. Además de poder compilarse con Lean, cada resultado incluye una configuración para Comparator con un segundo comprobador, Nanoda. Esa ruta permite verificar que la solución demuestra el mismo enunciado público, que no introduce axiomas inesperados y que la acepta más de un núcleo.

La redundancia no es un detalle ceremonial. El proyecto fija Lean 4.32.0, y la versión 4.32.1 corrigió un fallo de solidez del núcleo. La documentación de Lean especifica que la comprobación recomendada mediante Comparator no estaba afectada por aquel fallo; las configuraciones de OpenAI activan precisamente el comprobador adicional. La lección no es que el certificado quede invalidado, sino que «compila» no debe ser el final de una auditoría adversaria. El código público permite repetirla con una base de confianza más pequeña que la del sistema que generó la prueba.

Esto representa un avance práctico respecto de febrero. En el desafío First Proof, OpenAI presentó diez intentos informales para problemas de investigación y acabó reconociendo, tras comentarios externos, que uno que inicialmente consideraba probablemente correcto era erróneo. En mayo, otro modelo interno refutó la conjetura de Erdős sobre distancias unitarias y la demostración fue revisada por matemáticos externos. Ahora la empresa ensaya una tercera vía a escala de lote: argumento legible, formalización pública y herramientas para una repetición independiente.

Lo que Lean no decide

Un certificado formal comprueba exactamente el teorema que se le ha dado, dentro de las definiciones que se le han dado. No decide por sí solo que ese enunciado corresponde fielmente a la conjetura expresada en lenguaje matemático ordinario. Tampoco establece que un resultado sea nuevo, importante o bien explicado, ni revisa la bibliografía. Esas conexiones forman parte de la especificación y siguen necesitando especialistas.

Esta distinción es especialmente importante en una colección tan heterogénea. Un experto en empaquetamiento de esferas no puede validar por extensión el resultado sobre repetición cuántica; cada capítulo requiere una comunidad distinta. El propio archivo de metadatos del repositorio califica la revisión actual como realizada por agentes. OpenAI aporta mucho más que una nota de prensa, pero los manuscritos acaban de publicarse y aún no equivalen a diez artículos aceptados tras revisión independiente.

Los recorridos de razonamiento tampoco son un registro bruto del descubrimiento. Su resumen explica que otro modelo leyó las cadenas originales junto con los artículos terminados y reconstruyó cómo surgieron las ideas, incluidos desvíos y enfoques fallidos. Son útiles para comprender las pruebas; no permiten auditar por completo qué instrucciones recibió Astra, cuántos candidatos exploró ni cuánto trabajo de selección hicieron las personas.

Esa ausencia cambia la lectura de la cifra económica más llamativa. OpenAI estima que los tokens necesarios para encontrar las soluciones exitosas costarían unos 2.000 dólares a tarifas de la API de Sol. No es el coste total del resultado: no incluye entrenar Astra, el universo de problemas o intentos descartados, la preparación humana de 249 páginas, la formalización —cuyo registro público anota una semana— ni la revisión. Sin ese denominador, la cifra muestra que una ejecución exitosa puede ser barata; no mide la probabilidad de obtenerla ni permite reproducir la productividad del sistema.

Mi lectura es que el avance seguiría siendo importante aunque la revisión independiente encontrara errores en una parte de la colección. Una demostración corregible no vale lo mismo que una correcta, pero la capacidad relevante aquí es una cadena más amplia: sostener argumentos en áreas muy distintas, convertirlos en objetos formales enormes y exponerlos a comprobación pública. Si varios resultados sobreviven, el cuello de botella de ciertas áreas puede desplazarse desde proponer una ruta de prueba hacia escoger preguntas, formalizar bien su significado, reconocer ideas valiosas y revisar un volumen creciente de resultados.

No conviene extrapolar ese cambio sin límites. Las matemáticas ofrecen una señal de verificación excepcional: un comprobador puede rechazar un paso inválido sin realizar un experimento físico. En biología, química o medicina, una derivación coherente no sustituye datos nuevos ni resultados clínicos. Astra tampoco está disponible para que un laboratorio externo repita el proceso, de modo que hoy se pueden reproducir los certificados, pero no la capacidad de descubrimiento que los produjo.

La Declaración de Leiden sobre IA y matemáticas defiende a la vez la verificación independiente, la atribución y el juicio de la comunidad. Este lanzamiento responde parcialmente con pruebas, código y una atribución explícita al sistema. Mantiene otra tensión: los argumentos son abiertos, pero el modelo, la selección y el proceso completo siguen siendo propietarios.

Ésa es la frontera que merece seguirse. El acontecimiento no es que Lean haya convertido automáticamente diez anuncios en verdad, ni que Astra haya reemplazado a los matemáticos. Es que un laboratorio ha publicado una tanda de contribuciones que ya no pide confiar sólo en la elocuencia del modelo. Ahora la comunidad puede separar corrección lógica, fidelidad del enunciado, novedad y valor. Para una IA que pretende ampliar conocimiento, esa separación es parte del resultado, no un trámite posterior.

Fuentes

← Volver al diario