GPT-5.6 reportedly closes a derivative-free convex optimization gap

Sources: Lean verification repository, HN discussion, r/math thread
Summary: An r/math thread that reached the Hacker News front page at 253 points reports that GPT-5.6, given a roughly 10-page specialized prompt, produced a proof closing a long-open gap in derivative-free convex optimization: a near-quadratic Omega(d squared) deterministic lower bound for optimizing convex Lipschitz functions from exact function values, matching the complexity of a 30-year-old algorithm. Phillip Kerger (UC Berkeley) published a Lean 4 and mathlib formalization of the deterministic lower bound alongside a manuscript titled "Closing the Oracle-Complexity Gap in Derivative-Free Convex Optimization". The formalization is machine-checked. The result is not peer reviewed, and the manuscript does not itself attribute the proof to an AI model.
Comments: HN and r/math commenters noted the proof is Lean-verified but stressed it required substantial domain expertise and a heavily engineered prompt built on prior research, and treated the model's authorship as a community claim rather than an established fact.
Why it matters: It extends the run of machine-checked AI-assisted math claims after the GPT-5.6 Sol Ultra Cycle Double Cover proof and the Star Fleet Erdős solutions, where Lean verification raises confidence in the math while the extent of the AI contribution stays contested.