AI agents design optimization algorithms with Lean-checked runtime bounds
A new preprint reports a staged AI workflow that proposes black-box optimization algorithms, then uses Lean to check their expected-runtime analyses.
Designing an algorithm is not enough—the runtime argument has to survive
A preprint posted on October 26 describes an AI-driven workflow for a more demanding mathematical task than solving a supplied theorem: proposing a black-box optimization algorithm and producing a Lean-checked argument for its expected runtime. The paper focuses on evolutionary-algorithm problems, where a method queries an objective function while seeking an optimum.
A staged route from proposal to proof
The system separates the work into stages. A language-model agent first suggests an algorithm, but Lean-based guards reject designs that fail basic formal conditions. The agent then proposes a potential function and develops drift bounds—a standard way of turning measured progress toward a goal into an expected-time guarantee. Formal steps are retried in response to Lean feedback, so a run is only counted as complete when its stated bound checks in the formal system.
The author reports 12 completed runs out of 15 with frontier models across eight problem classes. Among the examples, the manuscript says the pipeline found a polynomial expected-runtime algorithm for the CycleUncover problem, where the cited classical (1+1) evolutionary algorithm has exponential runtime, and matched the known order on LeadingOnes. An ablation without the staged process reportedly tended to reproduce the seeded random-search baseline or leave proofs unfinished. These are author-reported results from an unreviewed preprint, not an independent confirmation of the algorithms, proofs, or novelty claims.
What Lean certifies—and what readers should still inspect
A successful Lean check is valuable evidence that the encoded definitions and runtime argument fit together. It does not automatically show that the formal model captures every practical feature of a real optimizer, or that a proposed method will outperform alternatives outside the specified black-box setting. The paper also says its source repository was still to be published when the preprint appeared, which limits immediate independent reproduction.
Still, the workflow points to an interesting shift for mathematical AI: instead of using experiments alone to select generated heuristics, an agent can be required to carry a machine-checkable complexity argument alongside its design. The hard question then moves upstream—to the modelling choices and the translation of the intended algorithm into its formal specification.