Landau's function is constant on arbitrarily long runs (Nicolas 1968)

Open

LandauFunction.landau_constant_on_long_runs

by Lucas · Oct 9, 2026 · Mathlib 0df444a (Lean v4.33.1)

landau-function

There are arbitrarily long sequences of consecutive integers on which Landau's function is constant: for every $m\in\mathbb N$ there exists $n\in\mathbb N$ such that

g(n)=g(n+1)=\dots=g(n+m).

This shows that $g$ , although of growth $e^{(1+o(1))\sqrt{n\ln n}}$ , has arbitrarily long plateaus.

Preamble

import Mathlib
import Definitions.Def_LandauFunction_landau

Formal statement

namespace LandauFunction
theorem landau_constant_on_long_runs :
    ∀ m : ℕ, ∃ n : ℕ, ∀ k ≤ m, landau (n + k) = landau n := by sorry
end LandauFunction

Source

J.-L. Nicolas, Sur l'ordre maximum d'un élément dans le groupe Sn des permutations, Acta Arith. 14 (1968) 315–332; as quoted in Wikipedia, "Landau's function", revision oldid=1303222269 (https://en.wikipedia.org/w/index.php?title=Landau%27s_function&oldid=1303222269), second paragraph, ref. [1].

Read-back

What the Lean code literally says, in plain math · Aristotle (Harmonic) — non-blind, same agent as the drafter

Non-blind read-back — not independent testimony. This read-back was written by the same agent (Aristotle, by Harmonic) that drafted the Lean statement below, with full knowledge of the source material and of the intended meaning. It is not a blind audit by an independent auditor, and no reviewer should treat it as independent evidence of faithfulness. It was produced at the explicit request of the proposal owner.

For every natural number $m$ there exists a natural number $n$ such that for every natural number $k$ with $k\le m$ ,

g(n+k)=g(n),

where $g$ is the maximal order of a permutation of an $n$ -element set (definition landau). Thus the $m+1$ consecutive values $g(n),g(n+1),\dots,g(n+m)$ coincide. The case $m=0$ is trivially satisfied by any $n$ ; nothing in the statement requires $n$ to be large or the run to be maximal.

Human review

Endorsed by Shuze Chen · Oct 10, 2026
Confirmed by the moderator at approval.
Endorsed by Lucas · Oct 10, 2026
Confirmed by the mission captain (proposal self-audit).

View graph