GPT-5.6 Sol helped formally verify a lower bound for a convex optimization problem that had been open since 1996
According to mathematician Phillip Kerger, GPT-5.6 Sol proposed a proof about the limits of optimization, and Lean verified the new lower bound
On July 14, Berkeley lecturer Phillip Kerger posted a preprint on a convex optimization problem in which an algorithm receives only numerical function values. Kerger says that GPT-5.6 Sol found the proof construction during a session lasting about 2.5 hours. An open Lean project verifies the new lower bound at a precisely specified accuracy.
Consider the problem of finding the lowest point of an unknown bowl in a space with d parameters. The algorithm chooses a point and receives one number, the height of the bowl at that point. It must choose each subsequent point from the history of these values. How many measurements are unavoidable before the algorithm can be guaranteed to approach the minimum?
At an accuracy on the order of 1/√d, Protasov’s 1996 method provided an algorithm requiring roughly d² log²d measurements. The proven lower bound was much weaker, at about d measurements. The gap between these estimates left open the possibility of a radically more efficient algorithm.
Kerger’s preprint states a new lower bound: every deterministic algorithm requires on the order of d²/log(d+1) queries in the worst case. Up to logarithmic factors, this nearly closes the previous gap.
This is where Lean enters the process. Lean is a language and software system for formally verifying proofs. Every line of a proof receives an exact logical type, and the system’s kernel checks whether each conclusion follows from the preceding steps. The open code applies this procedure specifically to the new lower bound. For every algorithm with a limited number of queries, it constructs an admissible convex function on which the algorithm fails to achieve the specified accuracy.
The Lean project verifies the lower bound. The upper bound from Protasov’s work, the matching formula for complexity, and the extension to mixed-integer problems remain in the manuscript. Mathematical reviewers will need to assess those claims.
On July 16, Holden Thorp, editor in chief of the Science journals, wrote that AI may produce more science than humans can verify. For arguments that can be expressed in strict formal logic, Lean supports a specific sequence: the model proposes a proof construction, the kernel verifies the precise statement, and mathematicians assess the problem formulation and the conclusions.