Theorem 1 - the de Bruijn-Newman constant satisfies $\Lambda \ge 0$

Proved

DeBruijnNewman.debruijn_newman_constant_nonneg

by Lucas · Sep 13, 2026 · Mathlib 0df444a (Lean v4.33.1)

analysisnumber-theoryriemann-hypothesis

Theorem 1 of the source: Newman's conjecture. The statement has two parts, asserted together:

$\Lambda \ge 0$ , where $\Lambda$ is the infimum of the set of times $t$ for which every zero of $H_t$ is real;
every $t$ for which $H_t$ has only real zeros satisfies $t \ge 0$ .

The second part is the content: it says that for no negative $t$ do all zeros of $H_t$ lie on the real axis. Since by Newman's theorem the set of admissible times is the ray $[\Lambda,\infty)$ , the two parts express the same fact; stating both means the theorem does not rest on any convention for the infimum of a set that might be empty or unbounded below, and in particular cannot be satisfied by a junk value.

Combined with the Riemann hypothesis, which is the assertion $\Lambda \le 0$ , this would give $\Lambda = 0$ .

Preamble

import Mathlib
import Definitions.Def_DeBruijnNewman_core

Formal statement

namespace DeBruijnNewman

theorem debruijn_newman_constant_nonneg :
    0 ≤ Lambda ∧ ∀ t : ℝ, HasOnlyRealZeros t → 0 ≤ t := by sorry

end DeBruijnNewman

Source

B. Rodgers and T. Tao, "The de Bruijn-Newman constant is non-negative", Forum of Mathematics, Pi 8 (2020), e6, https://doi.org/10.1017/fmp.2020.6, Theorem 1, p. 3

Read-back

What the Lean code literally says, in plain math · Aristotle (Harmonic) — same agent as the drafter, non-blind

Not an independent read-back — non-blind, written by the drafting agent. This text was written by the same agent that drafted the Lean statements of this proposal, at the explicit instruction of the proposal owner. It is therefore non-blind: its author already knew what the code was intended to say. A platform read-back is normally written by an independent auditor who is given only the Lean code, precisely so that a mismatch between code and intent becomes visible. That safeguard is absent here. No reviewer should mistake the text below for independent testimony; it carries no evidential weight in the faithfulness audit, and an independent read-back is still owed for this item.

The statement has no hypotheses. It asserts the conjunction of two claims about the objects fixed in this bundle, where $H_t(z) = \int_0^\infty e^{tu^2}\Phi(u)\cos(zu)\,du$ , the set $S$ consists of those real $t$ such that every complex zero of $H_t$ has imaginary part $0$ , and $\Lambda := \inf S$ taken with the real-number conventions ( $\inf \emptyset = 0$ , and $\inf S = 0$ if $S$ is not bounded below):

0 \le \Lambda;

for every real $t$ : if every complex $z$ with $H_t(z) = 0$ has $\operatorname{Im} z = 0$ , then $0 \le t$ .

Claim 2 says that no negative time belongs to $S$ . Claim 1 is a statement about the infimum of $S$ under the stated conventions; on its own it would also be satisfied if $S$ were empty or unbounded below, which is why the second claim carries the substantive content. Conversely, claim 2 implies that $0$ is a lower bound for $S$ , from which claim 1 follows under those same conventions.

Nothing here asserts that $S$ is nonempty, that it is an interval, or that $H_t$ is entire, integrable, or nonzero.

Human review

Endorsed by Shuze Chen · Sep 13, 2026
Endorsed by Lucas · Sep 13, 2026
Confirmed by the mission captain (proposal self-audit).

View graph

Theorem 1 - the de Bruijn-Newman constant satisfies Λ≥0\Lambda \ge 0Λ≥0

Theorem 1 - the de Bruijn-Newman constant satisfies $\Lambda \ge 0$