A computer-assisted bound Λ ≤ 0.107964910079 for the de Bruijn–Newman constant

In the Polymath normalisation, this preprint presents a computer-assisted proof of the unconditional bound Λ ≤ 427693072077942473661578098491/3961408125713216879677197516800 < 0.107964910079 for the de Bruijn–Newman constant. OpenAI’s ordinary-zeta nonvanishing theorem for Re(s) > 7/8 supplies the initial strip. That theorem is formalised in Lean; the included source is pinned to openai/math commit fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb. The subsequent proof combines written analytic estimates with exact rational and directed interval computations, including the full terminal de Bruijn contraction T + Q_T/2. Version 1.0 contains a 63-page main manuscript and matching LaTeX source, a matched-source supplement, a consequences note, a verification guide, two historical papers, and the proof and replay archive. Appendix B, Theorem B.1, directly reconstructs all 67 source chords. The included execution receipt records passing results for all 15 finite stages, including reconstruction of 268 final source fields and verification of 221,010 comparison arcs. Manifests and checksums identify the delivered files. This edition supersedes referee edition 3 of 28 October 2026; the numerical plan, source table and comparison history are unchanged; Appendix B adds the direct source reconstruction. The work develops the translated-probe programme in the author’s earlier records 10.5281/zenodo.22626161, 10.5281/zenodo.22867547 and 10.5281/zenodo.23272725. The imported Lean theorem, written analytic arguments and numerical checks have distinct scopes, documented in the manuscript and verification guide. This package does not claim a new full Lean rebuild or an end-to-end Lean formalisation of the final bound. AI assistants contributed to derivations, code, exposition and internal checks; Dale James Raymond remains responsible for the submission. CC BY 4.0 applies to author-owned publication documents. Included software and external theorem sources retain their applicable component-specific rights and licence terms, including MIT, LGPL-3.0-or-later and Apache-2.0. LICENSES_AND_RIGHTS.md specifies the scopes and corresponding-source provisions.

Authors

Publication Details

Journal
Zenodo (CERN European Organization for Nuclear Research)
Published
2026-10-29
DOI
https://doi.org/10.5281/zenodo.23752102
Primary Topic
Analytic Number Theory Research
Type
preprint
Controls
|||
ALL TIME
JAN
FEB
MAR
APR
MAY
JUN
JUL
AUG
SEP
OCT
preprint

A computer-assisted bound Λ ≤ 0.107964910079 for the de Bruijn–Newman constant

Dale James Raymond
2 links
Zenodo (CERN European Organization for Nuclear Research)
Analytic Number Theory Research
preprint

A computer-assisted bound Λ ≤ 0.107964910079 for the de Bruijn–Newman constant

Dale James Raymond
preprint en

Abstract

In the Polymath normalisation, this preprint presents a computer-assisted proof of the unconditional bound Λ ≤ 427693072077942473661578098491/3961408125713216879677197516800 < 0.107964910079 for the de Bruijn–Newman constant. OpenAI’s ordinary-zeta nonvanishing theorem for Re(s) > 7/8 supplies the initial strip. That theorem is formalised in Lean; the included source is pinned to openai/math commit fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb. The subsequent proof combines written analytic estimates with exact rational and directed interval computations, including the full terminal de Bruijn contraction T + Q_T/2. Version 1.0 contains a 63-page main manuscript and matching LaTeX source, a matched-source supplement, a consequences note, a verification guide, two historical papers, and the proof and replay archive. Appendix B, Theorem B.1, directly reconstructs all 67 source chords. The included execution receipt records passing results for all 15 finite stages, including reconstruction of 268 final source fields and verification of 221,010 comparison arcs. Manifests and checksums identify the delivered files. This edition supersedes referee edition 3 of 28 October 2026; the numerical plan, source table and comparison history are unchanged; Appendix B adds the direct source reconstruction. The work develops the translated-probe programme in the author’s earlier records 10.5281/zenodo.22626161, 10.5281/zenodo.22867547 and 10.5281/zenodo.23272725. The imported Lean theorem, written analytic arguments and numerical checks have distinct scopes, documented in the manuscript and verification guide. This package does not claim a new full Lean rebuild or an end-to-end Lean formalisation of the final bound. AI assistants contributed to derivations, code, exposition and internal checks; Dale James Raymond remains responsible for the submission. CC BY 4.0 applies to author-owned publication documents. Included software and external theorem sources retain their applicable component-specific rights and licence terms, including MIT, LGPL-3.0-or-later and Apache-2.0. LICENSES_AND_RIGHTS.md specifies the scopes and corresponding-source provisions.

Zenodo (CERN European Organization for Nuclear Research)
Analytic Number Theory Research
AI Navigator

Ask Laika to Summarize, Analyze, and Connect papers live on the map.

Summarize Papers & Methodologies

Extract key findings, datasets, and comparative methods across publications.

Benchmark Rankings & Visual Analytics

Rank top research institutions, authors, funders, topics, and journals by Field-Weighted Citation Impact (FWCI) and paper volume with instant charts.

Connect Distant Disciplines

Bridge topological clusters on the map to find hidden collaborative intersections.

Laika access coming soon
A computer-assisted bound Λ ≤ 0.107964910079 for the de Bruijn–Newman constant — Dale James Raymond · Zenodo (CERN European Organization for Nuclear Research) (2026) | TGRS Research Map | TGRS