Agentic Algorithm Design: LLMs that Propose, Formalise, and Prove Runtime Bounds for Evolutionary Algorithms in Lean

Recent progress in AI for mathematics demonstrates the strong capability of frontier LLMs to generate proofs for given mathematical statements. Whether these models are also capable of formulating useful new concepts and definitions, and of proving statements about them, is not yet clear. We focus on automating the design and analysis of randomised search heuristics for combinatorial optimisation and ask whether current AI agents are capable of inventing new algorithmic designs along with Lean proofs of their expected runtime. Modelled after the research methodology from runtime analysis of evolutionary algorithms, we formalise a pipeline for automated design and analysis of novel optimisation algorithms. To demonstrate the pipeline, we generate an optimisation algorithm for the linear pseudo-Boolean function class Onemax along with a formal proof that the algorithm has expected running time $O(n^3)$ on this problem class. The complete design and analysis synthesised by the agent comprises 2036 lines of Lean code. To rule out that the agent merely restates known algorithms and analyses, we also apply the pipeline to CycleUncover, a new problem on which the (1+1) EA needs exponential time. Here, the agent designs a learn-then-solve algorithm that is unlike any evolutionary algorithm, with a machine-checked expected runtime of $O(n^2)$ (2373 lines of Lean code), whereas the same model without the staged pipeline only produces random search. While the generated algorithms do not go beyond state-of-the-art human designs, this is to our knowledge the first example of automated design and analysis of randomised optimisation algorithms by agents. The fact that no previous Lean proofs for randomised optimisation algorithms have been published in the literature further strengthens the result. As a stand-alone contribution, we have developed the first Lean formalisation of drift analysis. In particular, drift analysis can yield bounds on the expected hitting times of a broad range of stochastic processes, including evolutionary algorithms (EAs). We provide a formalisation of the additive drift theorem from measure-theoretic foundations, derive from it the multiplicative drift theorem, and apply the latter to manually prove an asymptotically optimal $(1+o(1))en\ln(n)$ upper bound on the expected runtime of the (1+1) EA. While traditional pen-and-paper analyses of EAs gloss over some technical details and assumptions, our formalisation builds on rigorous measure theory and martingale theory.