Massias' bound $g(n)\le\exp(1.05314\sqrt{n\ln n})$

Open

LandauFunction.landau_le_massias

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

landau-function

For every natural number $n$ ,

g(n)\le\exp\!\left(1.05314\sqrt{n\ln n}\right).

This makes the upper half of Landau's theorem explicit, with a constant close to the asymptotically optimal value $1$ .

Formalization Note For $n=0,1$ the right-hand side is $1=g(n)$ .

Preamble

import Mathlib
import Definitions.Def_LandauFunction_landau

Formal statement

namespace LandauFunction
theorem landau_le_massias (n : ℕ) :
    (landau n : ℝ) ≤ Real.exp (1.05314 * Real.sqrt (n * Real.log n)) := by sorry
end LandauFunction

Source

J.-P. Massias, Ann. Fac. Sci. Toulouse Math. (5) 6 (1984) 269–281; as quoted in Wikipedia, "Landau's function", revision oldid=1303222269 (https://en.wikipedia.org/w/index.php?title=Landau%27s_function&oldid=1303222269), last display, ref. [5].

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)\le\exp\!\left(1.05314\cdot\sqrt{n\ln n}\right),

where $g(n)$ is the maximal order of a permutation of an $n$ -element set (definition landau), cast to a real number, $1.05314$ is the exact decimal $105314/100000$ , $\ln$ is the real natural logarithm (with $\ln 0=0$ ) and $\sqrt{\cdot}$ the real square root. For $n=0$ and $n=1$ the argument of $\exp$ is $0$ . No other 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

Massias' bound g(n)≤exp⁡(1.05314nln⁡n)g(n)\le\exp(1.05314\sqrt{n\ln n})g(n)≤exp(1.05314nlnn​)

Massias' bound $g(n)\le\exp(1.05314\sqrt{n\ln n})$