Motivation

The Riemann hypothesis concerns the zeros of a complex analytic function, yet it admits an equivalent formulation involving only positive integers, finite sums, the real exponential, and the natural logarithm. Jeffrey C. Lagarias established this formulation in An Elementary Problem Equivalent to the Riemann Hypothesis (Theorem 1.1). It connects the distribution of divisors of an integer with the analytic behavior of the zeta function. For number theorists and formalizers, the interest lies in making that connection precise without confusing an elementary statement with an elementary proof.

The objective is the known equivalence selected by LeanEval v1, not a resolution of RH. Lagarias's paper builds on results of Guy Robin concerning large values of the divisor-sum function; those results remain substantial parts of the formalization workload (Lagarias, §3).

Setting

For a positive integer $n$, its divisor sum is

$$\sigma(n)=\sum_{d\mid n}d,$$

where the sum runs over positive divisors, including $1$ and $n$. Its harmonic number is

$$H_n=\sum_{j=1}^{n}\frac1j.$$

All inequalities below are inequalities of real numbers. The symbols $\exp$ and $\log$ denote the real exponential and natural logarithm. The Euler–Mascheroni constant is $\gamma=\lim_{n\to\infty}(H_n-\log n)$.

The Riemann zeta function is obtained by analytic continuation of $\sum_{m=1}^{\infty}m^{-s}$ from $\operatorname{Re}(s)>1$. RH asserts that its nontrivial zeros have real part $1/2$. The Lagarias elementary criterion in this mission is the assertion that $\sigma(n)\le H_n+\exp(H_n)\log(H_n)$ for every positive integer $n$. These conventions agree with the arithmetic quantities in Lagarias, Problem E, with the precise equality-clause distinction stated below.

Formalization targets

Main goal: the exact LeanEval equivalence

$$\mathrm{RH}\quad\Longleftrightarrow\quad \forall n\in\mathbb N,\;n>0\Longrightarrow \sigma(n)\le H_n+\exp(H_n)\log(H_n).$$

There are no hypotheses on the goal theorem. The quantifier ranges over all positive integers, not a bounded test set or an unspecified tail. The benchmark uses a non-strict inequality and does not include an equality characterization. Lagarias's Problem E additionally requires equality only at $n=1$; the proof of the reverse implication in Theorem 1.1, p. 8 uses the non-strict inequality alone. The stronger source formulation is therefore not silently substituted for the benchmark.

Supporting targets from the paper

The milestone list records the following source statements, with their thresholds unchanged:

• Lemma 3.1: for $n\ge3$,

$$e^\gamma n\log\log n\le\exp(H_n)\log(H_n).$$

• Lemma 3.2: for $n\ge20$,

$$H_n+\exp(H_n)\log(H_n)\le e^\gamma n\log\log n+\frac{7n}{\log n}.$$

• The finite check in the proof of Theorem 1.1: the criterion holds for $1\le n\le5040$, with equality exactly at $n=1$.
• Proposition 3.1, attributed to Robin: assuming RH, for $n\ge5041$,

$$\sigma(n)\le e^\gamma n\log\log n.$$

• Proposition 3.2, attributed to Robin: if RH is false, some fixed $0<\beta<1/2$ and $C>0$ satisfy

$$\sigma(n)\ge e^\gamma n\log\log n+ \frac{Cn\log\log n}{(\log n)^\beta}$$

for arbitrarily large integers $n$.

All five are taken from Lagarias, §3, pp. 6–8; the finite check is explicitly an unnumbered step, not a newly attributed lemma.

Significance

The result identifies an exact arithmetic reformulation of RH. It does not make either side unconditional. A proof of the equivalence gives a bridge between statements in different mathematical languages; it does not certify the universal inequality merely because many instances can be checked. This distinction is central to the interpretation of Lagarias's theorem.

The formalization would connect existing Mathlib definitions of the zeta function, divisor sums, harmonic numbers, and Euler's constant through a machine-checked argument. Reusable outputs include explicit harmonic/exponential comparisons, certified finite real inequalities, and formal versions of Robin's conditional and oscillation results. The mathematical results are known; this proposal supplies open formalization targets, not completed proofs. No accepted LeanEval result is claimed by creating or launching the mission.

Difficulty

The elementary appearance of the criterion hides its main analytic requirements. Bounding the divisor sum crudely, or checking any finite number of integers, cannot establish the universal equivalence. The conditional upper bound and especially the quantitative oscillation theorem connect zeta zeros with unusually large divisor sums. They must be proved, not packaged as definitions or presumed available because the paper cites them (Lagarias, Propositions 3.1–3.2).

The oscillation statement requires uniform positive constants and arbitrarily large indices. Replacing it with one counterexample loses essential information. The bounded computation also requires rigorous control of exponential and logarithmic values: an ordinary floating-point loop is not a Lean proof. Beyond the listed milestones, completion still requires standard growth comparisons, threshold bookkeeping, and assembly of the two implications. The short length of the source's final argument should not be read as an estimate of total formalization effort.

Formalization scope

The goal is LeanEval.NumberTheory.riemann_hypothesis_iff_lagarias_elementary_criterion, with type RiemannHypothesis ↔ LagariasElementaryCriterion. The criterion definition is copied from the benchmark. σ 1 n is natural-valued and cast to the reals; harmonic n is rational-valued and cast to the reals. RH remains Mathlib's predicate on riemannZeta, excluding negative even trivial zeros and the point $s=1$. No replacement axiom, hidden RH assumption, altered zeta function, or circular child restatement is permitted.

The goal excludes $n=0$ and includes $n=1$. Thresholds ensure positive logarithm arguments in the analytic milestones. The oscillation milestone expresses an infinite subset of the naturals as an unbounded set, retaining $n\ge3$; deletion of the finitely many smaller indices does not change the source's infinitude claim. Its real exponent is represented by Real.rpow, not natural exponentiation. Constants are chosen before the arbitrary cutoff.

The benchmark pins Lean 4.33.0 and Mathlib 6f1ef4e5dd604a435bddba4747b13970cd65d2a1. The proposal targets Prove2me's supported Lean 4.33.1 environment, Mathlib 0df444a360eaa60ab8c11dca51a86af692955474. These environments are distinct; eventual benchmark credit requires the benchmark's own validation. Contributions to analytic infrastructure, source-faithful supporting results, and certified finite inequalities are welcome. The five milestones are an initial source-backed structure, not a claim that all required infrastructure is already present.

Selected references

• Jeffrey C. Lagarias, An Elementary Problem Equivalent to the Riemann Hypothesis, American Mathematical Monthly 109 (2002), 534–543. arXiv:math/0008177v2, posted 6 May 2001. The theorem, proposition, equation, and page numbers in this proposal refer to this nine-page arXiv version.
• Guy Robin, Grandes valeurs de la fonction somme des diviseurs et hypothèse de Riemann, Journal de Mathématiques Pures et Appliquées 63 (1984), 187–213. Bibliography entry [18] in Lagarias. The milestone formulations are those explicitly reproduced and attributed in Lagarias's Propositions 3.1 and 3.2.