Lagarias elementary criterion (exact LeanEval definition)

Definition

LeanEval_NumberTheory_LagariasElementaryCriterion

by xuanji · Sep 6, 2026 · Mathlib 0df444a (Lean v4.33.1)

lagariasnumber-theoryriemann-hypothesis

For a positive integer $n$ , let $\sigma(n)=\sum_{d\mid n}d$ and $H_n=\sum_{j=1}^n 1/j$ . The Lagarias elementary criterion is the proposition

\forall n\in\mathbb N,\quad n>0\Longrightarrow \sigma(n)\le H_n+\exp(H_n)\log(H_n).

This definition names an arithmetic assertion; it does not assume or define the Riemann hypothesis. The inequality is non-strict, includes $n=1$ , excludes $n=0$ , and has no equality-only clause. Harmonic numbers are rational numbers cast to the reals, and the natural-valued divisor sum is also cast to the reals.

Definition code

import Mathlib.NumberTheory.ArithmeticFunction.Misc
import Mathlib.NumberTheory.Harmonic.Defs
import Mathlib.NumberTheory.LSeries.RiemannZeta

namespace LeanEval.NumberTheory

open scoped ArithmeticFunction.sigma

def LagariasElementaryCriterion : Prop :=
  ∀ n : ℕ,
    0 < n →
      ((σ 1 n : ℕ) : ℝ) ≤
        (harmonic n : ℝ) +
          Real.exp (harmonic n : ℝ) * Real.log (harmonic n : ℝ)

end LeanEval.NumberTheory

Source

Jeffrey C. Lagarias, An Elementary Problem Equivalent to the Riemann Hypothesis, arXiv:math/0008177v2 (6 May 2001), https://arxiv.org/abs/math/0008177v2, p. 1, Problem E, equation (1.1); the non-strict inequality only, exactly as in LeanEval statement revision 1.

Read-back

What the Lean code literally says, in plain math · gpt-6-astra

The proposition LagariasElementaryCriterion is defined to mean that for every natural number $n$ , if $n>0$ , then $\sum_{d\mid n} d \le H_n+\exp(H_n)\log(H_n)$ , where the sum ranges over the positive divisors of $n$ , its natural-number value is viewed as a real number, and $H_n=\sum_{i=0}^{n-1}1/(i+1)$ is computed as a rational number and then viewed as a real number. Here $\exp$ is the real exponential and $\log$ is the natural logarithm; its argument satisfies $H_n\ge 1$ under the hypothesis. The quantification includes $n=0$ , but the implication imposes no inequality in that case because its hypothesis is false.

Human review

Endorsed by Shuze Chen · Sep 6, 2026
Endorsed by xuanji · Sep 6, 2026
Confirmed by the mission captain (proposal self-audit).

View graph