GPT-5.6 Sol Ultra produce una demostración de la Conjetura de Cobertura Doble del Ciclo [pdf]

Validez y verificación de la demostración

• Muchos están entusiasmados pero con cautela: la demostración es corta, usa teoría de grafos anterior a los años 90 y parece plausible, aunque podría contener errores sutiles.
• Algunos sostienen que debería haber sido anunciada por matemáticos profesionales o después de una formalización en Lean / revisión por pares en una revista.
• Otros señalan que OpenAI ha publicado un repositorio de formalización en Lean, pero las bibliotecas de teoría de grafos aún son inmaduras, por lo que mecanizarlo no es trivial.
• Varios comentaristas intentaron que otros LLM y herramientas revisaran la demostración; en general informan que no ven errores obvios, pero subrayan que eso no sustituye la revisión de expertos.
• Al menos una preocupación técnica planteada en Reddit se argumenta en el hilo como un problema de notación, no como un fallo fatal. Veredicto general: prometedora, pero todavía no aceptada universalmente.

Prompts, harness y conciencia del tiempo

• El prompt publicado es fuertemente meta: instruye al modelo a asumir que existe una demostración, trabajar durante al menos 8 horas, evitar informes de estado vagos y explorar múltiples estrategias.
• Los comentaristas ven esto como “hackeo de motivación” y guía de metaheurística más que como autonomía pura.
• Hay discusión sobre el seguimiento del tiempo en harnesses de agentes (marcas temporales, date del sistema operativo, herramientas de cuota) frente a la falta de sentido temporal innato de los modelos.
• Sol Ultra se describe como muchos subagentes en paralelo con razonamiento máximo, a diferencia del enfoque “best-of-N” de Sol Pro.

Opacidad metodológica y sesgo de supervivencia

• Varios comentaristas preguntan cuántos problemas y variantes de prompt se probaron, y cuántas ejecuciones fallidas precedieron a este éxito.
• Se especula que OpenAI ha estado ejecutando muchos problemas desde el resultado anterior de distancia unitaria; la ausencia de una “tasa de fracaso” dificulta medir la capacidad.
• Preocupa que las empresas destaquen los éxitos raros por marketing mientras ocultan los resultados nulos.

Importancia para las matemáticas y los asistentes de demostración

• Algunos lo ven como un hito importante: un modelo listo para usar resolviendo un famoso problema abierto en menos de una hora.
• Otros señalan que es una demostración de estilo “truco ingenioso”, no un avance de construcción teórica prolongada; argumentan que el siguiente listón es el desarrollo autónomo de teoría nueva sustancial.
• Hay un fuerte apoyo a avanzar hacia la verificación formal al estilo Lean para lidiar con grandes volúmenes de demostraciones generadas por IA y reducir los cuellos de botella de verificación humana.

Implicaciones más amplias y ansiedades

• Debate sobre qué tareas son más automatizables: cualquier cosa con corrección fácilmente comprobable (matemáticas, código, seguridad, algo de ciencia) puede ser especialmente vulnerable.
• Discusión filosófica sobre el valor de las matemáticas puras, si los resultados generados por IA “se sienten vacíos”, y qué sigue siendo exclusivamente humano (creación de conjeturas, gusto, explicación, responsabilidad).
• Algunos expresan preocupación por los empleos, el valor humano y el bombo de la IA; otros responden que el valor humano no está ligado a la productividad económica y que las herramientas ampliarán, no borrarán, a las personas.