Near-quadratic lower bound for derivative-free convex optimization
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.
- Lab
- Independent
- Model
- GPT-5.6 Sol Pro
- Field
- Mathematics
- Date
- 2026-07-14
- Human collaborators
- Phillip Kerger
- Problem posed
- 1996 · open 30 yrs
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 and known objections
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
Lean 4 / Mathlib compiler (author-run, artifact public): core Ω̃(d²) lower bound compiles with no sorry and no bespoke axioms · link ↗
Disagree with these grades?
Bring a citation: a grade moves on evidence, not on argument.
Or on GitHub: submit a check challenge the grade send a correction or send a pull request
Flag this for triage
Signals order the review queue and nothing else. They are never published, and they never move a grade: that takes a citation.
Entry history (1 event)
- AddedEntered the registry graded Formally verified and AI-led.
Entries are never deleted. A grade that does not hold up is downgraded on the record, with the reason beside it.
Graded formally verified for verification and ai-led for autonomy. What these mean.
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-boundBibTeX
@misc{whataifound-independent-2026-bound,
title = {Near-quadratic lower bound for derivative-free convex optimization},
author = {{whataifound.org}},
year = {2026},
howpublished = {whataifound.org: A Registry of AI Scientific and Mathematical Discoveries},
note = {Result by Independent. Verification: Formally verified. Autonomy: AI-led.},
url = {https://whataifound.org/finding/2026-07-14-zeroth-order-oracle-bound}
}