Lagarias criterion is equivalent to RH

riemann_hypothesis_iff_lagarias_elementary_criterion — a formalization challenge from the lean-eval benchmark.

Notes

Lagarias' elementary divisor-sum criterion stated using Mathlib's RiemannHypothesis, harmonic numbers, and sigma notation.

Formal statement

theorem riemann_hypothesis_iff_lagarias_elementary_criterion :
    RiemannHypothesis ↔ LagariasElementaryCriterion := by
  sorry

Informal solution sketch

Prove that the Riemann hypothesis is equivalent to the inequality σ(n) ≤ H_n + exp(H_n) log(H_n) for all positive integers n.

Source

https://arxiv.org/abs/math/0008177

How to submit

Challenge.lean and Solution.lean are part of the trusted benchmark and must not be modified. Write your proof in Submission.lean (plus any local modules under Submission/). Mathlib may be used freely; anything not in Mathlib has to be inlined into the submission.

Comparator configuration

• Solution module: Solution
• Theorems checked: riemann_hypothesis_iff_lagarias_elementary_criterion
• Permitted axioms: propext, Quot.sound, Classical.choice

Submitted by Kim Morrison.