Finite range and equality case through 5040

Proved

LeanEval.NumberTheory.lagarias_finite_range

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

lagariasnumber-theoryriemann-hypothesis

For each integer $1\le n\le5040$ , let $\sigma(n)$ be the sum of its positive divisors. Then

\sigma(n)\le H_n+\exp(H_n)\log(H_n),

and equality holds if and only if $n=1$ . This is the bounded verification reported in the proof of Theorem 1.1, not the universal criterion. Its formal proof must certify the real exponential and logarithm comparisons; floating-point evidence alone is insufficient.

Preamble

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

open scoped ArithmeticFunction.sigma

Formal statement

namespace LeanEval.NumberTheory

theorem lagarias_finite_range (n : ℕ) (hn : 0 < n) (hbound : n ≤ 5040) :
    (((σ 1 n : ℕ) : ℝ) ≤ (harmonic n : ℝ) +
      Real.exp (harmonic n : ℝ) * Real.log (harmonic n : ℝ)) ∧
      ((((σ 1 n : ℕ) : ℝ) = (harmonic n : ℝ) +
      Real.exp (harmonic n : ℝ) * Real.log (harmonic n : ℝ)) ↔ n = 1) := by sorry

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. 8, proof of Theorem 1.1, finite verification (unnumbered).

Read-back

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

For every natural number $n$ with $0<n\le 5040$ , let $\sigma_1(n)=\sum_{d\mid n,\ d>0}d$ be the sum of its positive divisors and let $H_n=\sum_{j=1}^{n}1/j$ , regarded as a real number. Then $\sigma_1(n)\le H_n+\exp(H_n)\log(H_n)$ , and $\sigma_1(n)=H_n+\exp(H_n)\log(H_n)$ if and only if $n=1$ , where $\exp$ is the real exponential and $\log$ is the natural logarithm. The range includes both $n=1$ and $n=5040$ and excludes $n=0$ ; throughout this range $H_n>0$ .

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