Un hilo de r/math reporta que GPT-5.6 usó un prompt inspirado en la prueba del problema CDC de OpenAI para atacar un problema abierto de optimización convexa desde hace 30 años. La prueba resultante fue formalizada y verificada línea por línea en Lean, sin marcadores de pasos sin demostrar.
