Berkeley researcher used GPT-5.6 to derive a Lean-verified optimization bound
Phillip Kerger's preprint narrows a gap dating to 1996, though the paper remains unreviewed and Lean covers only its lower-bound result.
By Ryan Merket · Published
Primary source: Reddit
Why it matters
The result shows frontier models can turn expert-scaffolded prompts into publishable mathematical arguments, while formal proof systems are becoming essential credibility infrastructure.
Phillip Kerger, an assistant teaching professor at UC Berkeley, used OpenAI's GPT-5.6 Sol Pro to produce the central argument for a new lower bound in convex optimization, then formalized the result in the Lean theorem prover.
Kerger submitted the 36-page preprint on July 14th. In a July 15th account, he said the model returned its initial proof after 148 minutes of uninterrupted work. The paper has not been peer reviewed.…