$\ln g(n)=\sqrt{\mathrm{Li}^{-1}(n)}+O(R(\sqrt{n\ln n})\ln n)$ (Massias–Nicolas–Robin 1988)

Proved

LandauFunction.landau_log_eq_sqrt_logIntegralInv

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

asymptoticslandau-functionprime-number-theorem

Let $c>0$ and put $R(x)=x\exp\!\left(-c(\ln x)^{3/5}(\ln\ln x)^{-1/5}\right)$ . If $\pi(x)-\mathrm{Li}(x)=O(R(x))$ as $x\to\infty$ , then, as $n\to\infty$ ,

\ln g(n)=\sqrt{\mathrm{Li}^{-1}(n)}+O\!\left(R\bigl(\sqrt{n\ln n}\bigr)\ln n\right).

Combined with Ford's error term this holds unconditionally for some $c>0$ ; it expresses $\ln g(n)$ through the inverse logarithmic integral.

Formalization Note The hypothesis on $\pi-\mathrm{Li}$ is stated with the same $c$ as the conclusion, as in the source; $R$ is written out explicitly in both places.

Preamble

import Mathlib
import Definitions.Def_LandauFunction_landau
import Definitions.Def_LandauFunction_logIntegral

Formal statement

namespace LandauFunction
theorem landau_log_eq_sqrt_logIntegralInv (c : ℝ) (hc : 0 < c)
    (hπ : (fun x : ℝ => (Nat.primeCounting ⌊x⌋₊ : ℝ) - logIntegral x) =O[Filter.atTop]
      (fun x : ℝ => x * Real.exp (-c * Real.log x ^ ((3 : ℝ) / 5) *
        Real.log (Real.log x) ^ (-(1 : ℝ) / 5)))) :
    (fun n : ℕ => Real.log (landau n) - Real.sqrt (logIntegralInv n)) =O[Filter.atTop]
      (fun n : ℕ =>
        (Real.sqrt (n * Real.log n) *
          Real.exp (-c * Real.log (Real.sqrt (n * Real.log n)) ^ ((3 : ℝ) / 5) *
            Real.log (Real.log (Real.sqrt (n * Real.log n))) ^ (-(1 : ℝ) / 5))) *
        Real.log n) := by sorry
end LandauFunction

Source

Massias, Nicolas, Robin, Acta Arith. 50 (1988) 221–242; as quoted in Wikipedia, "Landau's function", revision oldid=1303222269 (https://en.wikipedia.org/w/index.php?title=Landau%27s_function&oldid=1303222269), display "ln g(n) = sqrt(Li^{-1}(n)) + O(R(sqrt(n ln n)) ln n)", ref. [3].

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.

Let $c$ be a real number with $c>0$ , and for real $x$ write

R_c(x)=x\exp\!\left(-c\,(\ln x)^{3/5}(\ln\ln x)^{-1/5}\right)

(real powers; $\ln$ the real logarithm). Hypothesis: as $x\to+\infty$ over the reals, $\pi(\lfloor x\rfloor)-\mathrm{Li}(x)=O(R_c(x))$ , where $\pi(m)$ counts primes $\le m$ , $\lfloor x\rfloor$ is the natural-number floor, and $\mathrm{Li}(x)=\int_2^x dt/\ln t$ (definition logIntegral).

Conclusion: as $n\to\infty$ through the natural numbers,

\ln g(n)-\sqrt{\mathrm{Li}^{-1}(n)}=O\!\left(R_c\!\left(\sqrt{n\ln n}\right)\cdot\ln n\right),

where $g(n)$ is the maximal order of a permutation of an $n$ -element set (definition landau), $\mathrm{Li}^{-1}(y)=\inf\{x\ge2: y\le\mathrm{Li}(x)\}$ (definition logIntegralInv, which for $y\ge 0$ is the inverse of $\mathrm{Li}$ on $[2,\infty)$ ), and $\sqrt{\cdot}$ is the real square root (which returns $0$ on negative input). The same $c$ appears in hypothesis and conclusion. The statement is universally quantified over $c>0$ ; it is only informative for those $c$ for which the hypothesis holds.

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

ln⁡g(n)=Li−1(n)+O(R(nln⁡n)ln⁡n)\ln g(n)=\sqrt{\mathrm{Li}^{-1}(n)}+O(R(\sqrt{n\ln n})\ln n)lng(n)=Li−1(n)​+O(R(nlnn​)lnn) (Massias–Nicolas–Robin 1988)

$\ln g(n)=\sqrt{\mathrm{Li}^{-1}(n)}+O(R(\sqrt{n\ln n})\ln n)$ (Massias–Nicolas–Robin 1988)