Lagarias criterion is equivalent to RH

Open

LeanEval.NumberTheory.riemann_hypothesis_iff_lagarias_elementary_criterion

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

lagariasnumber-theoryriemann-hypothesis

The Riemann hypothesis is equivalent to the assertion that, for every positive integer $n$ ,

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

where $\sigma(n)=\sum_{d\mid n}d$ and $H_n=\sum_{j=1}^n1/j$ . This is the exact LeanEval v1 target: both directions of the equivalence, with no hypotheses, no finite cutoff, and no equality-only clause. It asks for formalization of a known equivalence, not a proof that RH or the universal arithmetic criterion holds.

Source distinction. Lagarias's Problem E also specifies equality only at $n=1$ . The goal deliberately uses the weaker non-strict criterion required by the benchmark; the reverse argument on p. 8 needs only this inequality.

Preamble

import Definitions.Def_LeanEval_NumberTheory_LagariasElementaryCriterion

Formal statement

namespace LeanEval.NumberTheory

theorem riemann_hypothesis_iff_lagarias_elementary_criterion :
    RiemannHypothesis ↔ LagariasElementaryCriterion := 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. 1, Theorem 1.1 and Problem E, equation (1.1); p. 8, proof using only the non-strict inequality for the reverse implication. Exact goal: LeanEval/NumberTheory/Lagarias.lean, statement revision 1.

Read-back

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

The assertion that every complex number $s$ satisfying $\zeta(s)=0$ , $s\ne 1$ , and $s\ne -2(m+1)$ for every natural number $m\ge 0$ has real part $\operatorname{Re}(s)=\tfrac12$ , where $\zeta$ is the Riemann zeta function, is equivalent to the following assertion: for every natural number $n>0$ , $\sum_{d\mid n,\ d>0}d\le H_n+\exp(H_n)\log(H_n)$ , where the sum runs over the positive divisors of $n$ , $H_n=\sum_{j=1}^{n}1/j$ , and the inequality is in the real numbers. The latter assertion imposes no condition at $n=0$ ; for every permitted $n$ , $H_n>0$ , so $\log(H_n)$ is the ordinary real natural logarithm.

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