Landau's theorem: $\ln g(n)\sim\sqrt{n\ln n}$

Proved

LandauFunction.landau_log_tendsto

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

asymptoticslandau-function

Landau's function satisfies

\lim_{n\to\infty}\frac{\ln g(n)}{\sqrt{n\ln n}}=1,

equivalently $g(n)=e^{(1+o(1))\sqrt{n\ln n}}$ .

This determines the growth rate of the largest order of an element of the symmetric group $S_n$ .

Formalization Note The limit is along $n\to\infty$ in $\mathbb N$ ; at $n=0,1$ the denominator is $0$ and Lean's division gives $0$ , which does not affect the limit.

Preamble

import Mathlib
import Definitions.Def_LandauFunction_landau

Formal statement

namespace LandauFunction
theorem landau_log_tendsto :
    Filter.Tendsto (fun n : ℕ => Real.log (landau n) / Real.sqrt (n * Real.log n))
      Filter.atTop (nhds 1) := by sorry
end LandauFunction

Source

E. Landau (1902/1903); as quoted in Wikipedia, "Landau's function", revision oldid=1303222269 (https://en.wikipedia.org/w/index.php?title=Landau%27s_function&oldid=1303222269), third paragraph, first display, ref. [2].

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.

As $n\to\infty$ through the natural numbers,

\frac{\ln g(n)}{\sqrt{n\ln n}}\longrightarrow 1,

where $g(n)$ is the maximal order of a permutation of an $n$ -element set (definition landau), cast to a real number, $\ln$ is the real natural logarithm and $\sqrt{\cdot}$ the real square root. Division by $0$ is defined to give $0$ , which happens exactly for $n=0,1$ (where $n\ln n=0$ ); since the statement is a limit, these finitely many values play no role. No hypotheses.

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

Landau's theorem: ln⁡g(n)∼nln⁡n\ln g(n)\sim\sqrt{n\ln n}lng(n)∼nlnn​

Landau's theorem: $\ln g(n)\sim\sqrt{n\ln n}$