Qué publicó OpenAI el 1 de agosto
El 1 de agosto de 2026 OpenAI hizo públicas diez demostraciones de problemas abiertos de matemáticas y de informática teórica, obtenidas por una versión interna de un modelo al que la compañía llama Astra. El material son dos cosas: un manuscrito de 249 páginas y el repositorio openai/ten-proofs en GitHub, con un certificado en Lean 4 por resultado, licencia Apache 2.0 y recuento de sorry igual a cero, es decir, ningún paso sin demostrar.
Astra no está disponible: no hay fecha de lanzamiento ni precio, no está confirmado si será GPT-6 o una variante de la familia GPT-5, y queda pendiente una revisión federal de seguridad previa. Lo único público es el resultado.
Los diez resultados
El titular es la primera construcción explícita de un grupo no sófico, la pregunta que Mikhail Gromov dejó abierta al introducir la soficidad en 1999 y llevaba veintisiete años sin respuesta. Le siguen un contraejemplo a la conjetura de rigidez de Connes sobre álgebras de von Neumann, planteada en 1980, y una demostración de la conjetura del volumen de Ehrhart.
El resto reparte entre geometría, teoría de códigos y complejidad: la primera mejora de la cota superior general de empaquetamiento de esferas desde 1978, cotas para códigos binarios y esféricos, una cota inferior de complejidad de circuitos para el permanente, repetición paralela en juegos cuánticos de dos jugadores, dureza de aproximación del vector más cercano en retículos y contraejemplos en teoría extremal de grafos. Tres salen del catálogo de Erdős, entre ellos el 183, sobre números de Ramsey multicolor.