Near-quadratic lower bound for derivative-free convex optimization

Near-quadratic lower bound for derivative-free convex optimization is graded formally verified on whataifound.org, with the AI's role graded ai-led.

A lower bound of order d²/log d on the number of exact function evaluations needed to minimize a convex Lipschitz function, closing a gap open since 1996 and showing a 1996 algorithm was essentially optimal.

Verification

Formally verified

Autonomy

AI-led

Lab

Independent

Model

GPT-5.6 Sol Pro

Field

Mathematics

Date

2026-07-14

Human collaborators

Phillip Kerger

Problem posed

1996 · open 30 yrs

Notability

17 Wikipedia language editions

What was found

In zeroth-order optimization an algorithm may only query a function's value, never its gradient. Protasov's 1996 algorithm needed about d² evaluations in d dimensions, but the best known lower bound was only about d, leaving open whether a much faster method existed. The new bound of Ω(d²/log(d+1)) matches the upper bound to polylogarithmic factors. Kerger reports that after a ten-page prompt built on his own earlier failed attempts, the model produced the complete proof in a single 2.5-hour session with no intervention; he then reviewed it and formally verified the core bound in Lean 4, which compiles against Mathlib with no `sorry` and no bespoke axioms.

Novelty check

The gap between Protasov's O(d²) upper bound (1996) and the O(d) lower bound is documented in the derivative-free optimization literature and had stood for three decades. No prior matching lower bound appears in the literature. The paper is explicit that the AI produced the argument.

Caveats

arXiv preprint, not peer-reviewed. The author states plainly that 'it is accurate to say that the AI model used solved the problem, not the author of this paper', which is the basis for the ai-led grade; the human wrote the prompt, reviewed the proof, and did the Lean formalization. Graded `formal` on the strength of the machine-checked Lean artifact for the core bound, not on the preprint as a whole.

Independent checks

Sources

How this is graded

whataifound.org grades every entry on two axes: verification (how solid the result is, from a machine-checked proof down to refuted) and autonomy (how much the AI did versus its human collaborators). This finding is formally verified and ai-led. Full definitions are in the methodology.

Cite this entry

whataifound.org (2026). Near-quadratic lower bound for derivative-free convex optimization. whataifound.org: A Registry of AI Scientific and Mathematical Discoveries. https://whataifound.org/finding/2026-07-14-zeroth-order-oracle-bound

← All mathematics findings in the registry