Riemann hypothesis criterion via Landau's function

Open

LandauFunction.landau_riemann_hypothesis_iff

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

landau-functionriemann-hypothesis

The inequality

\ln g(n)<\sqrt{\mathrm{Li}^{-1}(n)}

holds for all sufficiently large $n$ if and only if the Riemann hypothesis is true.

This is an elementary reformulation of the Riemann hypothesis in terms of element orders in symmetric groups; it is included as a faithful statement of the source, not as an expected deliverable.

Formalization Note The Riemann hypothesis is Mathlib's RiemannHypothesis; $\mathrm{Li}$ is the offset logarithmic integral (using $\mathrm{li}$ instead changes $\mathrm{Li}^{-1}(n)$ by $O(\ln n)$ ).

Preamble

import Mathlib
import Definitions.Def_LandauFunction_landau
import Definitions.Def_LandauFunction_logIntegral

Formal statement

namespace LandauFunction
theorem landau_riemann_hypothesis_iff :
    (∀ᶠ n : ℕ in Filter.atTop, Real.log (landau n) < Real.sqrt (logIntegralInv n)) ↔
      RiemannHypothesis := by sorry
end LandauFunction

Source

Massias, Nicolas, Robin, Acta Arith. 50 (1988); as quoted in Wikipedia, "Landau's function", revision oldid=1303222269 (https://en.wikipedia.org/w/index.php?title=Landau%27s_function&oldid=1303222269), sentence "The statement that ln g(n) < sqrt(Li^{-1}(n)) for all sufficiently large n is equivalent to the Riemann hypothesis".

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.

The statement is a logical equivalence between two propositions.

There exists $N\in\mathbb N$ such that for every natural number $n\ge N$ ,

\ln g(n)<\sqrt{\mathrm{Li}^{-1}(n)},

where $g(n)$ is the maximal order of a permutation of an $n$ -element set (definition landau), $\ln$ is the real natural logarithm, $\sqrt{\cdot}$ the real square root, and $\mathrm{Li}^{-1}(y)=\inf\{x\ge2: y\le\int_2^x dt/\ln t\}$ (definition logIntegralInv; for $y\ge 0$ it is the inverse of the offset logarithmic integral on $[2,\infty)$ ).

The Riemann hypothesis, as formulated in Mathlib (RiemannHypothesis): every zero $s$ of the Riemann zeta function that is not a trivial zero ( $s\ne -2,-4,-6,\dots$ ) and satisfies $s\ne1$ has real part $1/2$ .

The statement asserts (1) $\iff$ (2), with no further 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).
Endorsed by pitimespi · Nov 3, 2026
Confirmed by the mission captain (proposal self-audit).

View graph