Motivation

Landau's function $g(n)$ is the largest order of any permutation of $n$ objects. It is a basic invariant of the symmetric group $S_n$, and because the order of a permutation is the least common multiple of its cycle lengths, $g(n)$ is also the largest least common multiple of the parts of a partition of $n$. That second description ties a purely group-theoretic quantity to the distribution of prime numbers, which is why $g(n)$ has been studied as a meeting point of combinatorics and analytic number theory for over a century.

The interest of this mission is one sharp statement: an elementary inequality for $g(n)$ that is equivalent to the Riemann hypothesis. It gives a reformulation of the hypothesis that mentions no zeta function, no complex analysis, and no primes directly — only orders of permutations and the inverse logarithmic integral.

Timeline.

• 1902–1903. E. Landau proved $\ln g(n) \sim \sqrt{n \ln n}$.
• 1968. J.-L. Nicolas showed that $g$ is constant on arbitrarily long runs of consecutive integers.
• 1984. J.-P. Massias proved the explicit bound $\ln g(n) \le 1.05313836\sqrt{n \ln n}$ for all $n \ge 1$.
• 1988. J.-P. Massias, J.-L. Nicolas, and G. Robin obtained a three-term asymptotic expansion of $\ln g(n)$, expressed $\ln g(n)$ through the inverse logarithmic integral, and proved that a one-sided inequality for $\ln g(n)$ is equivalent to the Riemann hypothesis.
• 2002. K. Ford's bounds for the Riemann zeta function give a prime number theorem error term that can be fed into the 1988 result.

Setting

For a natural number $n$, let $S_n$ be the group of all permutations of an $n$-element set. The order of $\sigma \in S_n$ is the least $k \ge 1$ with $\sigma^k = \mathrm{id}$. Landau's function is

$$g(n) = \max_{\sigma \in S_n} \operatorname{ord}(\sigma).$$

The logarithmic integral is $\mathrm{Li}(x) = \int_2^x \frac{dt}{\ln t}$, and $\mathrm{Li}^{-1}$ is its inverse on $[2, \infty)$: for $y \ge 0$, $\mathrm{Li}^{-1}(y)$ is the least $x \ge 2$ with $y \le \mathrm{Li}(x)$. The Chebyshev functions are $\psi(x) = \sum_{n \le x} \Lambda(n)$ and $\theta(x) = \sum_{p \le x} \ln p$, where $\Lambda$ is the von Mangoldt function. The Riemann hypothesis is Mathlib's RiemannHypothesis: every non-trivial zero of the Riemann zeta function has real part $1/2$.

Formalization targets

Goal

$$\ln g(n) < \sqrt{\mathrm{Li}^{-1}(n)} \quad \text{for all sufficiently large } n \iff \text{the Riemann hypothesis}.$$

This is the goal theorem: the Massias–Nicolas–Robin criterion. It is the weakest stable statement of the criterion — it asserts the eventual inequality, not any particular constant or error term, so it survives improvements to the surrounding estimates.

The attack path

The milestones below it are the steps of the classical argument, in dependency order: the prime-power structure of $g(n)$ as a knapsack optimum; the transfer of error bounds between the Chebyshev functions; the expression of $\ln g(n)$ through $\mathrm{Li}^{-1}$; and the two analytic directions that connect the Riemann hypothesis to the error term of $\psi$.

Significance

The result itself. The criterion is one of the few known elementary reformulations of the Riemann hypothesis: it replaces a statement about complex zeros with a statement about finite groups and one real integral. A proof of the criterion in either direction passes through the explicit formula linking prime distribution to zeta zeros, so formalizing it forces the development of that machinery in Lean — machinery that is reusable far beyond this mission, for the prime number theorem, zero-density estimates, and explicit prime bounds.

Formalizing it. Several steps are already machine-checked on the platform and Proved: the prime-power decomposition of $g(n)$, the transfer of a $\psi$-error bound to a $\theta$-error bound, the three-term asymptotic expansion of $\ln g(n)$, and the expression of $\ln g(n)$ through $\mathrm{Li}^{-1}$ under a prime-counting error hypothesis. What remains open is the analytic core: the implication from the Riemann hypothesis to the von Koch error bound for $\psi$, and the oscillation forced on $\psi$ when the hypothesis fails. The goal theorem itself is Open. Nothing in this mission is presented as open that is already closed, and nothing already Proved is re-proposed as a draft.

Relation to the existing catalog. The goal theorem is already listed as a milestone of the mission "Landau's Function: Growth of the Maximal Order of a Permutation", which treats the growth of $g(n)$ broadly across several papers. This mission is narrower: it makes the criterion itself the goal and assembles the dedicated attack path for its proof — the knapsack structure, the Chebyshev transfer, and the two analytic directions — which the broader mission does not list. The two missions share theorems; they do not duplicate each other's purpose.

Difficulty

The central difficulty is the gap between the combinatorial and analytic sides. On the combinatorial side, $g(n)$ is a finite optimum, computable in principle for each $n$. On the analytic side, the criterion is an asymptotic statement about all large $n$, governed by the zeros of $\zeta$. The obvious first idea — compare $g(n)$ directly with $\sqrt{\mathrm{Li}^{-1}(n)}$ for the $n$ one can compute — says nothing about the eventual inequality, because the two sides cross on a scale no computation reaches. The bridge has to go through the prime distribution: the optimum is governed by the Chebyshev functions at a threshold near $\sqrt{\mathrm{Li}^{-1}(n)}$, and the Chebyshev functions are governed by the zeta zeros. Each of those two links is a substantial formalization in its own right, and the second requires the explicit formula together with a zero-count bound.

Formalization scope

The Lean development uses the platform's definitions: landau is the supremum of orderOf over all permutations of Fin n, and logIntegralInv is the infimum definition of $\mathrm{Li}^{-1}$ above. The goal quantifies over all sufficiently large $n$ (Filter.atTop), not over all $n$ — the inequality is false for small $n$, and any formalization that dropped the "eventually" qualifier would state a different, false theorem. The $\psi$-error milestone is stated as an implication with the Riemann hypothesis as hypothesis, not as an unconditional bound; the oscillation milestone is stated with an explicit constant and an arbitrary $\varepsilon > 0$, matching the classical $\Omega_{\pm}$ statement, rather than with a hard-coded constant that the proof does not deliver. No milestone is weakened because it looks hard: the analytic directions are stated in full strength.

Contributions are welcome at every open milestone, and at the supporting bridge between the two formalizations of $g(n)$ used on the platform. The reusable infrastructure — the knapsack characterization of $g(n)$, the Chebyshev transfer, and the $\mathrm{Li}^{-1}$ expression — is already Proved and can be imported directly.

Selected references

• J.-P. Massias, J.-L. Nicolas, G. Robin, Évaluation asymptotique de l'ordre maximum d'un élément du groupe symétrique, Acta Arithmetica 50 (1988). https://doi.org/10.4064/aa-50-3-221-242
• H. von Koch, Sur la distribution des nombres premiers, Acta Mathematica 24 (1901). https://doi.org/10.1007/BF02403071
• E. Landau, Über die Maximalordnung der Permutationen gegebenen Grades, Archiv der Mathematik und Physik 5 (1903).
• Landau's function, Wikipedia. https://en.wikipedia.org/wiki/Landau%27s_function
• Sequence A000793 (maximal order of a permutation of $n$ elements), OEIS. https://oeis.org/A000793