Berkeley researcher used GPT-5.6 to derive a Lean-verified optimization bound

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.

The result concerns deterministic zeroth-order convex optimization, where an algorithm can evaluate a convex function at chosen points but receives no gradients or other information. This model applies when each evaluation comes from a simulator, physical experiment or other system that reveals only an outcome.

For convex, one-Lipschitz functions over a d-dimensional unit ball, the previously applicable lower bound required on the order of d evaluations. A method dating to 1996 supplied an upper bound of O(d^2 log^2 d) evaluations. Kerger's paper establishes a lower bound of Omega(d^2 / log(d+1)) at accuracy on the order of d^(-1/2), closing the dimension gap up to logarithmic factors.

That qualification matters. The paper does not prove that exactly d^2 evaluations are necessary, as some summaries of the work have suggested. It establishes a near-quadratic lower bound against a near-quadratic upper bound, leaving logarithmic factors between them. The theorem still rules out the possibility that a deterministic function-value-only method could generally match the previously known linear lower bound.

The prompt contained a year of domain work

Kerger was positioned to formulate the problem precisely. He earned a PhD in applied mathematics from Johns Hopkins University, where he studied optimization, algorithms and complexity, and previously worked on distributed quantum algorithms at NASA's Quantum Artificial Intelligence Laboratory. His earlier research includes lower bounds and information complexity for convex and mixed-integer optimization.

Kerger said he had worked on the problem sporadically for roughly a year. Earlier sessions with GPT-5.4 and GPT-5.5 failed to complete the proof, even when he steered those models toward the same broad family of hard functions that appeared in the final result.

The successful run began with a prompt about 10 pages long, included as an appendix to the preprint. Kerger modeled its structure on a prompt OpenAI released for its work on the Cycle Double Cover Conjecture. His version specified the mathematical setting, listed plausible approaches, supplied ideas from his earlier attempts and defined results that would not count as a solution.

Kerger also used GPT-5.6 to help synthesize related work and develop parts of that prompt. The 148-minute figure therefore measures the final uninterrupted proof-search session, rather than the full research effort that made the session possible. Kerger's prior work determined the question, constrained the search space and provided the standards the output had to meet.

The original shared conversation produced the main construction and proof argument at a stricter, less practically relevant accuracy setting. A later session helped refine the result to the d^(-1/2) accuracy stated in the preprint.

Lean verifies the central lower bound

Kerger published a Lean 4 repository alongside the paper. The repository contains the original d^(-3) result and a formalization of the sharper d^(-1/2) deterministic lower bound.

The formal theorem constructs a max-affine objective that defeats any deterministic exact-value strategy operating within the specified query budget. The repository checks convexity, one-Lipschitz behavior, consistency with the oracle transcript, the existence of a minimizer in the unit ball and the claimed objective gap.

The repository also draws a clear scope boundary: its Lean development verifies the deterministic lower-bound theorem. The known upper bound and the paper's transfer of the result to mixed-integer optimization remain outside the formalization.

Lean's kernel checks that a proof establishes the theorem encoded in the formal statement. That removes many opportunities for a plausible-looking argument to conceal an invalid step. Independent review still has to assess whether the formal statement faithfully captures the intended claim, whether the supporting literature has been interpreted correctly and whether the result is genuinely new.

Kerger's release provides the materials needed for that review: the paper, full prompt, model transcripts, source code, proof map, build instructions and a comparator configuration for checking the formal proof. The package is a stronger disclosure standard than a paper that merely credits an AI system in its acknowledgments.

The work also captures the division of labor emerging in AI-assisted mathematics. Kerger supplied the open question, accumulated the failed approaches, built the search instructions and audited the result. GPT-5.6 performed a long proof search and found the construction that completed the argument. Lean supplied the mechanical check that the encoded lower-bound proof holds together.