An $O(\mu{}n)$ runtime bound for the $(\mu+1)$ GA on $\mathrm{Jump}_k$ with crossover probability 1

lax-343628·formalized by Timo Kötzing · Christian Wallisch · GPT 6.1 Sol · Claude Opus 5.5·registered·created 30 Oct 2026·GitHub @155199a·Lean v4.33.0 epoch · mathlib db584cd6d46c

Loading review…

Abstract

For the $(\mu+1)$ genetic algorithm (GA) on $\mathrm{Jump}_k$ with constant crossover probability, the best previously known upper bound on the expected optimization time is $O(n^{k-1})$ for $k\ge3$ , attained for suitably chosen population sizes. This formalization establishes that, for small jump sizes, the $(\mu+1)$ GA without diversity mechanisms optimizes $\mathrm{Jump}_k$ in expected time $O(\mu n)$ with crossover probability $1$ , and more generally with every constant crossover probability $p_c\in(0,1]$ . The bound holds for jump sizes $k\le c\ln\ln n$ and population sizes $Ck(\ln n)^2\le\mu\le n^{O(1)}$ , where $c>0$ is a sufficiently small and $C$ a sufficiently large constant. It also holds for $k\le c\ln n$ and $n^{\varepsilon}\le\mu\le n^{O(1)}$ , where $\varepsilon>0$ is an arbitrary constant.

The proof was found, and the result formalized in Lean, using GPT 6.1 Sol and Claude Opus 5.5.

Concepts

thm✓LogJumpSizes
thm✓LogLogJumpSizes

defAlgorithm
defRuntime

Concept map

4 concepts

100%

Proven claimDefinitionThis submissionA → B: B builds on A

Proofs

Proof networkview on GitHub

100%

premise files concept fileProven claimClaim from this submissionAll proofs of one concept — hover for individual statements and proofs

Proof list

no assumptions

thm✓Lax343628.LogJumpSizes

⊢Lax343628Proofs.LogJumpSizes.runtime_bound
no assumptions

thm✓Lax343628.LogLogJumpSizes

⊢Lax343628Proofs.LogLogJumpSizes.runtime_bound

Lean sources for these proofs: proofs/ on GitHub

Proof code is not displayed; the archive records each proof's checked relationship between claims.

Related submissions

No other submission in the archive builds on this one, and this one builds on none.

Cite this

This is only the formalizers. The authors of the formalized results may be different (see References).

@misc{lax-343628,
  author = {Timo Kötzing and Christian Wallisch and GPT 6.1 Sol and Claude Opus 5.5},
  title = {An $O(\mu{}n)$ runtime bound for the $(\mu+1)$ GA on $\mathrm{Jump}_k$ with crossover probability 1},
  year = {2026},
  howpublished = {Lax Archive, lax-343628},
  url = {https://laxarchive.org/lax-343628/},
}

References

Thomas Jansen and Ingo Wegener. The Analysis of Evolutionary Algorithms—A Proof That Crossover Really Can Help. Algorithmica 34(1):47–66, 2002. doi:10.1007/s00453-002-0940-2
Duc-Cuong Dang, Tobias Friedrich, Timo Kötzing, Martin S. Krejca, Per Kristian Lehre, Pietro S. Oliveto, Dirk Sudholt and Andrew M. Sutton. Escaping Local Optima with Diversity Mechanisms and Crossover. In Proceedings of the Genetic and Evolutionary Computation Conference (GECCO 2016) 645–652, 2016. doi:10.1145/2908812.2908956
Duc-Cuong Dang, Tobias Friedrich, Timo Kötzing, Martin S. Krejca, Per Kristian Lehre, Pietro S. Oliveto, Dirk Sudholt and Andrew M. Sutton. Escaping Local Optima Using Crossover With Emergent Diversity. IEEE Transactions on Evolutionary Computation 22(3):484–497, 2018. doi:10.1109/TEVC.2017.2724201
Benjamin Doerr, Aymen Echarghaoui, Mohammed Jamal and Martin S. Krejca. Runtime Analysis of the $(\mu+1)$ GA: Provable Speed-Ups from Strong Drift towards Diverse Populations. In Proceedings of the AAAI Conference on Artificial Intelligence 38(18):20683–20691, 2024. doi:10.1609/aaai.v38i18.30055
Andre Opris, Johannes Lengler and Dirk Sudholt. Achieving Tight $O(4^k)$ Runtime Bounds on $\mathrm{Jump}_k$ by Proving that Genetic Algorithms Evolve Near-Maximal Population Diversity. Algorithmica 87(11):1564–1619, 2025. doi:10.1007/s00453-025-01323-x

Discussion

Ask a question or add context. Endorsements and structured flags are kept in the review panel above.

Loading discussion…

Lax Lean Archive

An $O(\mu{}n)$ runtime bound for the $(\mu+1)$ GA on $\mathrm{Jump}_k$ with crossover probability 1

Flags

Flag this submission