Landau's function as the maximal lcm of a partition

Proved

LandauFunction.landau_eq_sup_partition_lcm

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

landau-functionpartitions

For every natural number $n$ , Landau's function equals the largest least common multiple of the parts of a partition of $n$ :

g(n)=\max_{\lambda\vdash n}\operatorname{lcm}(\lambda_1,\dots,\lambda_k),

where $\lambda=(\lambda_1,\dots,\lambda_k)$ ranges over all partitions of $n$ into positive parts.

This is the bridge between the group-theoretic definition of $g$ and its arithmetic study.

Formalization Note Partitions are Mathlib's Nat.Partition n; the lcm of the empty partition of $0$ is $1$ .

Preamble

import Mathlib
import Definitions.Def_LandauFunction_landau

Formal statement

namespace LandauFunction
theorem landau_eq_sup_partition_lcm (n : ℕ) :
    landau n = (Finset.univ : Finset (Nat.Partition n)).sup fun p => p.parts.lcm := by sorry
end LandauFunction

Source

Wikipedia, "Landau's function", revision oldid=1303222269 (https://en.wikipedia.org/w/index.php?title=Landau%27s_function&oldid=1303222269), first paragraph ("Equivalently, g(n) is the largest least common multiple (lcm) of any partition of n").

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 $n$ :

g(n)=\sup_{\lambda}\operatorname{lcm}(\lambda),

where $g(n)$ is the maximum order of a permutation of $\{0,\dots,n-1\}$ (definition landau: the supremum of the orders of all such permutations), $\lambda$ ranges over all partitions of $n$ , i.e. all finite multisets of positive integers whose sum is $n$ , and $\operatorname{lcm}(\lambda)$ is the least common multiple of the multiset's elements (with the convention that the lcm of the empty multiset is $1$ ). The supremum is taken in $\mathbb N$ (least element $0$ ) over the finite set of all partitions of $n$ , which is nonempty for every $n$ ; for $n=0$ the only partition is the empty one, so the right-hand side is $1$ . No hypothesis on $n$ is imposed.

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