RiemannHypothesisEquivalents.lean`

Explanation legend Lean4 Domain Explanation Language (L4DEL)

L4DEL explanations are a separate layer. They do not change the Lean source. Intuition is explanatory prose; numbered items are a reading path; sources link the wording back to evidence.

L4DEL: Lean4 Domain Explanation Language

Annotation provenance. This overlay contains 10 curated AI-written annotations and 7190 mechanical source-derived annotations. They have not been human-reviewed as explanations; treat them as unverified and not mathematical authority. Retained generation history: The 71 original curated annotations were produced in a Claude Sonnet 5.5 session at medium effort; Claude Opus 5.5 is recorded in that session as the advisor model, not the direct author. The bulk source-derived expansion was generated mechanically from pinned source comments by tooling developed in a GPT-5.6 Sol session at ultra reasoning; GPT-5.6 Sol did not originate the quoted source prose. On 2026-10-17 the mechanically generated source-comment annotations of the Formal Conjectures, Carleson, FLT, PFR, CompFiles, Mathematics in Lean and Theorem Proving in Lean overlays were regenerated by the same generator after three corrections made in a Claude Sonnet 5.5 session: titles no longer cut a sentence inside mathematics or end on a dangling word, workflow markers are removed from the quoted prose, and declaration names follow the scanner's namespace resolution. The boilerplate step line was dropped, and comments that were only a row of dashes no longer yield annotations. No new prose was written and no human review is claimed.

Credit: The upstream authors and contributors retain credit for the project and mathematics. lean4-explainer only renders their pinned source and adds the separately disclosed explanation layer.

Project sources: Pinned project documentation, Formal Conjectures paper, arXiv v1

19 declarations, 10 contain sorry, 0 declared as axioms

Equivalents to the Riemann Hypothesis

This file contains formal statements that are known to be equivalent to the Riemann Hypothesis, following the survey [Co26], §4. The statement of the Riemann Hypothesis itself is in FormalConjectures.Millennium.RiemannHypothesis.

References:

[Co26] A. Connes, The Riemann Hypothesis: Past, Present and a Letter Through Time, 2026.

Imports (1)

FormalConjecturesUtil

theorem RiemannHypothesis.robin_criterion Robin's Criterion sorry line 46 source
Source documentation
Robin's Criterion. The Riemann Hypothesis is equivalent to $$ \sigma(n) < e ^ {\gamma} n\log\log n $$ for all $n > 5040$, where $\gamma$ is the Euler-Mascheroni constant and $\sigma(n)$ is the sum of divisors.

depends on sorry what this means
Statement uses: Iff, RiemannHypothesis, Nat, GT.gt, OfNat.ofNat, LT.lt, Real, ArithmeticFunction, ArithmeticFunction.sigma, HMul.hMul, Real.exp, Real.eulerMascheroniConstant, Real.log
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
22 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem robin_criterion :
    RiemannHypothesis ↔ ∀ n > 5040, σ 1 n < (exp eulerMascheroniConstant) * n * log (log n) := by
…
```
theorem RiemannHypothesis.robin_criterion_rhs The statement that Robin's criterion holds sorry line 52 source
Source documentation
The statement that Robin's criterion holds.

depends on sorry what this means
Statement uses: Nat, GT.gt, OfNat.ofNat, LT.lt, Real, ArithmeticFunction, ArithmeticFunction.sigma, HMul.hMul, Real.exp, Real.eulerMascheroniConstant, Real.log
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
22 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem robin_criterion_rhs {n : ℕ} (hn : n > 5040) :
    σ 1 n < exp eulerMascheroniConstant * n * log (log n) := by
…
```
theorem RiemannHypothesis.lagarias_criterion Lagarias' Criterion sorry line 67 source
Source documentation
Lagarias' Criterion. A refinement of Robin's criterion: the Riemann Hypothesis is equivalent to $$ \sigma(n) < H_n + e^{H_n}\log H_n $$ for all $n \geq 2$, where $H_n = 1 + 1/2 + \cdots + 1/n$ is the $n$th harmonic number.
Note that [Co26] states this for all $n \geq 1$, but at $n = 1$ both sides equal $1$; Lagarias' original formulation is the non-strict inequality for all $n \geq 1$, with equality only at $n = 1$.

depends on sorry what this means
Statement uses: Iff, RiemannHypothesis, Nat, GT.gt, OfNat.ofNat, LT.lt, Real, ArithmeticFunction, ArithmeticFunction.sigma, HAdd.hAdd, harmonic, HMul.hMul, Real.exp, Real.log
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
30 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem lagarias_criterion : RiemannHypothesis ↔
    ∀ n > 1, σ 1 n < harmonic n + exp (harmonic n) * log (harmonic n) := by
…
```
theorem RiemannHypothesis.lagarias_criterion_rhs The statement that Lagarias' criterion holds sorry line 73 source
Source documentation
The statement that Lagarias' criterion holds.

depends on sorry what this means
Statement uses: Nat, LT.lt, OfNat.ofNat, Real, ArithmeticFunction, ArithmeticFunction.sigma, HAdd.hAdd, harmonic, HMul.hMul, Real.exp, Real.log
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
30 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem lagarias_criterion_rhs {n : ℕ} (hn : 1 < n) :
    σ 1 n < harmonic n + exp (harmonic n) * log (harmonic n) := by
…
```
def RiemannHypothesis.nontrivialPosZeros The nontrivial zeros of the Riemann zeta function with positive imaginary part line 79 source
Source documentation
The nontrivial zeros of the Riemann zeta function with positive imaginary part. Since the nontrivial zeros are closed under complex conjugation, these determine all nontrivial zeros.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Set, Complex
Proof uses: Set.ofPred, And, LT.lt, Real, OfNat.ofNat, Complex.re, Complex.im, Eq, riemannZeta
6 instances, coercions and auxiliary constants left out.
```
def nontrivialPosZeros : Set ℂ := {z | 0 < z.re ∧ z.re < 1 ∧ 0 < z.im ∧ riemannZeta z = 0}
```
def RiemannHypothesis.lambda Documented declaration: lambda line 93 source
Source documentation
The numbers $$ \lambda_n := \sum_{\rho}\left(1 - \left(1 - \frac{1}{\rho}\right)^n\right) $$ appearing in Li's criterion, summing over the nontrivial zeros $\rho$ of the Riemann zeta function.
This is a real number because nontrivial zeros always come in conjugate pairs. Note that, as stated, the sum is only conditionally convergent, however it is absolutely convergent when taken in conjugate pairs, since $1/\rho + 1/\bar\rho = 2\Re\rho/|\rho|^2$. Hence we sum over the zeros with positive imaginary part with summand 2 * (_).re, which makes the unordered sum ∑' meaningful.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real
Proof uses: tsum, Complex, RiemannHypothesis.nontrivialPosZeros, HMul.hMul, OfNat.ofNat, Complex.re, HSub.hSub, HPow.hPow, HDiv.hDiv, Membership.mem, Set, SummationFilter.unconditional
24 instances, coercions and auxiliary constants left out.
```
noncomputable def lambda (n : ℕ) : ℝ := ∑' ρ : nontrivialPosZeros, 2 * (1 - (1 - 1 / ρ.1) ^ n).re
…
```
Mentions: RiemannHypothesis.nontrivialPosZeros
theorem RiemannHypothesis.li_criterion Li's Criterion sorry line 102 source
Source documentation
Li's Criterion. The Riemann Hypothesis is equivalent to the positivity of $$ \lambda_n := \sum_{\rho}\left(1 - \left(1 - \frac{1}{\rho}\right)^n\right) $$ for each $n > 0$.

depends on sorry what this means
Statement uses: Iff, RiemannHypothesis, Nat, GT.gt, OfNat.ofNat, LT.lt, Real, RiemannHypothesis.lambda
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
10 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem li_criterion : RiemannHypothesis ↔ ∀ n > 0, 0 < lambda n := by
…
```
Mentions: RiemannHypothesis.lambda
theorem RiemannHypothesis.li_criterion_rhs The statement that Li's criterion holds sorry line 107 source
Source documentation
The statement that Li's criterion holds.

depends on sorry what this means
Statement uses: Nat, LT.lt, OfNat.ofNat, Real, RiemannHypothesis.lambda
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
10 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem li_criterion_rhs {n : ℕ} (hn : 0 < n) : 0 < lambda n := by sorry
```
Mentions: RiemannHypothesis.lambda
def RiemannHypothesis.fractScalarInv The function $\rho_{\theta} := \left\{\frac{\theta}{x}\right\}$ appearing in the Beurling-Nyman criterion line 111 source
Source documentation
The function $\rho_{\theta} := \left\{\frac{\theta}{x}\right\}$ appearing in the Beurling-Nyman criterion.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real
Proof uses: Int.fract, HDiv.hDiv
6 instances, coercions and auxiliary constants left out.
```
noncomputable def fractScalarInv (θ : ℝ) (x : ℝ) : ℝ := Int.fract (θ / x)
…
```
theorem RiemannHypothesis.aEStronglyMeasurable_fractScalarInv line 114 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, MeasureTheory.AEStronglyMeasurable, RiemannHypothesis.fractScalarInv, MeasureTheory.MeasureSpace.volume
Proof uses: Measurable.aestronglyMeasurable, Function.comp, Int.fract, HDiv.hDiv, id, Measurable.comp, measurable_fract, Measurable.div, measurable_const, measurable_id
54 instances, coercions and auxiliary constants left out.
theorem RiemannHypothesis.fractScalarInv_memLp2 line 118 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, MeasureTheory.MemLp, RiemannHypothesis.fractScalarInv, OfNat.ofNat, ENNReal, Nat, MeasureTheory.Measure.restrict, MeasureTheory.MeasureSpace.volume, Set.Ioc
Proof uses: MeasureTheory.MemLp.of_bound, MeasureTheory.AEStronglyMeasurable.restrict, RiemannHypothesis.aEStronglyMeasurable_fractScalarInv, Filter.Eventually.of_forall, LE.le, Norm.norm, MeasureTheory.ae, MeasureTheory.Measure, Eq.mpr, abs, id, Eq, congrArg, Real.norm_eq_abs, abs_of_nonneg, Int.fract_nonneg, HDiv.hDiv, LT.lt.le, Int.fract, Int.fract_lt_one
71 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
def RiemannHypothesis.fractScalarInvSumL2 The linear combination $\sum_{\nu = 1}^n c_{\nu}\rho_{\theta_\nu}$ expressed explicitly as an element of $L^2(0, 1)$ line 127 source
Source documentation
The linear combination $\sum_{\nu = 1}^n c_{\nu}\rho_{\theta_\nu}$ expressed explicitly as an element of $L^2(0, 1)$.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, Real, Subtype, MeasureTheory.AEEqFun, MeasureTheory.Measure.restrict, MeasureTheory.MeasureSpace.volume, Set.Ioc, OfNat.ofNat, Membership.mem, AddSubgroup, MeasureTheory.Lp, ENNReal
Proof uses: Finset.sum, Finset.univ, HSMul.hSMul, MeasureTheory.MemLp.toLp, RiemannHypothesis.fractScalarInv
72 instances, coercions and auxiliary constants left out.
```
noncomputable def fractScalarInvSumL2 (n : ℕ) (c θ : Fin n → ℝ) :
    Lp ℝ 2 (volume.restrict (Set.Ioc (0 : ℝ) 1)) :=
…
```
Mentions: c
theorem RiemannHypothesis.beurling_nyman_criterion Beurling-Nyman Criterion sorry line 136 source
Source documentation
Beurling-Nyman Criterion. The Riemann Hypothesis is equivalent to the statement that the set of finite linear combination $\sum_{\nu = 1}^n c_{\nu}\rho_{\theta_{\nu}}$ is dense in $L^2(0, 1)$, when ranging over $0 < \theta_{\nu}\leq 1$ and $\sum_{\nu = 1}^n c_{\nu}\theta_{\nu} = 0$.

depends on sorry what this means
Statement uses: Iff, RiemannHypothesis, Dense, Subtype, MeasureTheory.AEEqFun, Real, MeasureTheory.Measure.restrict, MeasureTheory.MeasureSpace.volume, Set.Ioc, OfNat.ofNat, Membership.mem, AddSubgroup, MeasureTheory.Lp, ENNReal, Nat, Set.ofPred, Exists, Fin, Set, Eq and 4 more
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
64 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem beurling_nyman_criterion : RiemannHypothesis ↔
    Dense { fractScalarInvSumL2 n c θ | (n) (c) (θ)
      (hθ : ∀ ν, θ ν ∈ Set.Ioc 0 1) (h : ∑ ν, c ν * θ ν = 0) } := by
…
```
Mentions: RiemannHypothesis.fractScalarInvSumL2, c
theorem RiemannHypothesis.beurling_nyman_criterion_rhs The statement that the Beurling-Nyman criterion holds sorry line 143 source
Source documentation
The statement that the Beurling-Nyman criterion holds.

depends on sorry what this means
Statement uses: Dense, Subtype, MeasureTheory.AEEqFun, Real, MeasureTheory.Measure.restrict, MeasureTheory.MeasureSpace.volume, Set.Ioc, OfNat.ofNat, Membership.mem, AddSubgroup, MeasureTheory.Lp, ENNReal, Nat, Set.ofPred, Exists, Fin, Set, Eq, Finset.sum, Finset.univ and 2 more
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
64 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem beurling_nyman_criterion_rhs :
    Dense { fractScalarInvSumL2 n c θ | (n) (c) (θ)
      (hθ : ∀ ν, θ ν ∈ Set.Ioc 0 1) (h : ∑ ν, c ν * θ ν = 0) } := by
…
```
Mentions: RiemannHypothesis.fractScalarInvSumL2, c
def RiemannHypothesis.weilArchimedean The additive Archimedean factor appearing in the Weil criterion line 149 source
Source documentation
The additive Archimedean factor appearing in the Weil criterion.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real
Proof uses: HAdd.hAdd, HMul.hMul, Real.log, OfNat.ofNat, Real.pi, Real.eulerMascheroniConstant, MeasureTheory.integral, MeasureTheory.Measure.restrict, MeasureTheory.MeasureSpace.volume, Set.Ioi, HDiv.hDiv, HSub.hSub, Neg.neg, Real.exp
24 instances, coercions and auxiliary constants left out.
```
noncomputable def weilArchimedean (f : ℝ → ℝ) : ℝ :=
…
```
def RiemannHypothesis.weilNonArchimedean The additive non-Archimedean factor appearing in the Weil criterion line 154 source
Source documentation
The additive non-Archimedean factor appearing in the Weil criterion.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real
Proof uses: HMul.hMul, Real.log, tsum, Real.exp, HDiv.hDiv, Neg.neg, HAdd.hAdd, OfNat.ofNat, SummationFilter.unconditional
18 instances, coercions and auxiliary constants left out.
```
noncomputable def weilNonArchimedean (p : ℕ) (f : ℝ → ℝ) : ℝ :=
…
```
def RiemannHypothesis.IsTestFunction The additive condition on test functions line 160 source
Source documentation
The additive condition on test functions. The property in [Co26] that $\hat{g}(\pm i/2) = 0$, where $\hat{g}$ is the Mellin transform, corresponds to the vanishing of the Fourier transform at $\pm 1/2$.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real
Proof uses: And, Eq, MeasureTheory.integral, MeasureTheory.MeasureSpace.volume, HMul.hMul, Real.exp, HDiv.hDiv, OfNat.ofNat, Neg.neg
18 instances, coercions and auxiliary constants left out.
```
def IsTestFunction (g : ℝ → ℝ) : Prop := ∫ x, g x * exp (x / 2) = 0 ∧ ∫ x, g x * exp (-x / 2) = 0
…
```
theorem RiemannHypothesis.weil_positivity_criterion Weil's Positivity Criterion sorry line 173 source
Source documentation
Weil's Positivity Criterion. The Riemann Hypothesis is equivalent to the non-positivity of Weil factor sums on the convolution of test functions. In [Co26] this is expressed as $$ \sum_v W_v(g\star g^*) \leq 0 $$ for all compactly-supported smooth functions $g : \mathbb{R}_+^{\times} \to \mathbb{C}$ such that the Mellin transform of $g$ vanishes at $\pm i / 2$, where $g^*(x) := \bar{g}(x^{-1})$ and $W_v$ are the multiplicative Weil factors defined in [Co26]. We formalise this as the corresponding additive statement (via $x = e^u$), since convolution in mathlib is additive, and restrict to real-valued test functions $g$, which suffices for the equivalence.

depends on sorry what this means
Statement uses: Iff, RiemannHypothesis, CompactlySupportedContinuousMap, Real, ContDiff, ENat, Top.top, RiemannHypothesis.IsTestFunction, LE.le, HAdd.hAdd, RiemannHypothesis.weilArchimedean, MeasureTheory.convolution, Neg.neg, ContinuousLinearMap.lsmul, MeasureTheory.MeasureSpace.volume, tsum, Nat.Primes, RiemannHypothesis.weilNonArchimedean, Nat, Nat.Prime and 2 more
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
81 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem weil_positivity_criterion :
    RiemannHypothesis ↔ ∀ g : C_c(ℝ, ℝ), ContDiff ℝ ∞ g → IsTestFunction g →
      weilArchimedean (g ⋆ fun x ↦ g (-x)) +
        ∑' p : Nat.Primes, weilNonArchimedean p (g ⋆ fun x ↦ g (-x)) ≤ 0 := by
…
```
Mentions: RiemannHypothesis.IsTestFunction, RiemannHypothesis.weilArchimedean, RiemannHypothesis.weilNonArchimedean
theorem RiemannHypothesis.weil_positivity_criterion_rhs The statement that the Weil criterion holds sorry line 181 source
Source documentation
The statement that the Weil criterion holds.

depends on sorry what this means
Statement uses: CompactlySupportedContinuousMap, Real, ContDiff, ENat, Top.top, RiemannHypothesis.IsTestFunction, LE.le, HAdd.hAdd, RiemannHypothesis.weilArchimedean, MeasureTheory.convolution, Neg.neg, ContinuousLinearMap.lsmul, MeasureTheory.MeasureSpace.volume, tsum, Nat.Primes, RiemannHypothesis.weilNonArchimedean, Nat, Nat.Prime, SummationFilter.unconditional, OfNat.ofNat
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
81 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem weil_positivity_criterion_rhs {g : C_c(ℝ, ℝ)} (hg : ContDiff ℝ ∞ g)
    (h : IsTestFunction g) :
    weilArchimedean (g ⋆ fun x ↦ g (-x)) +
      ∑' p : Nat.Primes, weilNonArchimedean p (g ⋆ fun x ↦ g (-x)) ≤ 0 := by
…
```
Mentions: RiemannHypothesis.IsTestFunction, RiemannHypothesis.weilArchimedean, RiemannHypothesis.weilNonArchimedean