Complete resultmathematics · convex optimization
GPT-5.6 closes a zeroth-order convex-optimization gap
A 148-minute run using a CDC-style prompt produced the main quadratic lower-bound argument; Phillip Kerger checked and formally verified it, then obtained a stronger refinement in a later chat.
Editorial context
What happened
This is a particularly strong prompt-transfer case: a researcher explicitly adapted the Cycle Double Cover orchestration style to a different mathematical domain and preserved the resulting run.
Keep in view
The result was new and not peer reviewed at the research cutoff; the human researcher selected the problem, authored the elaborate prompt, checked the proof, and formalized it.
Chronology
Timeline
Original uninterrupted 148-minute runattempt · day date
Preprint, prompts, chats, and Lean repository shareddisclosure · day date
Trust boundaries
Validation
Author-reviewed Lean formalization; not yet peer reviewed at cutoff.
System
AI and tools
- GPT-5.6 Sol Pro
- Lean
People
Human contributors
- Phillip Kerger
Organizations
Affiliations
- UC Berkeley
Primary materials