de_bruijn_newman_constant
Disprovedmillennium-prizenumber-theory
The de Bruijn–Newman constant Λ: The Riemann Hypothesis is equivalent to Λ ≤ 0. It is known that 0 ≤ Λ (Rodgers–Tao 2018, proving Λ ≥ 0 refuted the conjecture that Λ < 0). Proving Λ = 0 would prove RH. The question whether Λ = 0 is equivalent to but distinct from RH.
Preamble
import Mathlib
Formal statement
import Mathlib
theorem de_bruijn_newman_constant :
∃ (Lambda : ℝ),
Lambda = 0 ∧
∀ (t : ℝ), t < Lambda →
∃ (z : ℂ), z.re > 0 ∧
∑' (n : ℕ), Complex.exp (-t * (n : ℂ)^2 * Real.pi) *
(2 * Real.pi * (n : ℝ)^2 - 3) *
Complex.exp (-(n : ℂ)^2 * Real.pi) = 0 := by
sorrySource