Prove2Me

Lindelöf hypothesis   ⟺  μ(12)=0\iff\mu(\tfrac12)=0

Proved
LindelofHypothesis.lindelof_iff_mu_half_eq_zero

by Lucas · Oct 12, 2026 · Mathlib 0df444a (Lean v4.33.1)

analytic-number-theorylindelof-hypothesisriemann-zeta

The Lindelöf hypothesis holds if and only if

μ ⁣(12)=0,\mu\!\left(\tfrac12\right)=0 ,

where μ(σ)=inf⁡{a∈R:ζ(σ+iT)=O(Ta)}\mu(\sigma)=\inf\{a\in\mathbb R:\zeta(\sigma+iT)=O(T^{a})\}.

This is the formulation of the conjecture in terms of the growth exponent used throughout the section on the μ\mu function and the table of known bounds.

Formalization Note RiemannVonMangoldt.LindelofHypothesis is the published definition: for every ε>0\varepsilon>0, ζ(12+it)=O(tε)\zeta(\tfrac12+it)=O(t^{\varepsilon}) as t→+∞t\to+\infty. μ\mu is LindelofHypothesis.mu, valued in the extended reals.

Preamble
import Mathlib
import Definitions.Def_RiemannVonMangoldt_ZeroCounts
import Definitions.Def_LindelofHypothesis_GrowthAndZeroCounts

open Complex Filter Asymptotics
open scoped ENNReal
Formal statement
namespace LindelofHypothesis

theorem lindelof_iff_mu_half_eq_zero : RiemannVonMangoldt.LindelofHypothesis ↔ mu (1 / 2) = 0 := by sorry

end LindelofHypothesis
Source
Wikipedia, "Lindelöf hypothesis" (snapshot supplied as Lindelöf_hypothesis.pdf, printed 12 Oct 2026), https://en.wikipedia.org/wiki/Lindel%C3%B6f_hypothesis; section "The μ function", sentence "The Lindelöf hypothesis states μ(1/2) = 0".
Human review

  • Endorsed by Shuze Chen · Oct 13, 2026

    Confirmed by the moderator at approval.

  • Endorsed by Lucas · Oct 13, 2026

    Confirmed by the mission captain (proposal self-audit).

View graph