GPT-5.6 Sol Pro Closes 30-Year Gap in Zeroth-Order Convex Optimization, Lean-Verified in One Session

UC Berkeley IEOR teaching professor Phillip Kerger says GPT-5.6 Sol Pro proved that d² function evaluations are necessary for zeroth-order convex optimization — closing a 30-year gap between Protasov's 1996 d² upper bound and the prior best d lower bound. The model produced the proof in a single 2.5-hour session from a 10-page prompt, and the argument was machine-verified in Lean.