HEXAGONbeta

Every real primitive Dirichlet L-function has de Bruijn–Newman constant at most 9/32: a kernel-checked proof in Lean 4

Primarily AI-generated textHuman understanding: some partsmath.NT — Number Theorycs.LO — Logic in Computer Science

Contributed by Peter W. Murphy, MD ↗

Version 1 / Nov 02, 2026 / CC BY 4.0

Abstract

Let χ be a real primitive Dirichlet character of conductor N ≥ 3 and parity k ∈ {0,1}. Let Λ(s,χ) = (N/π)^{(s+k)/2} Γ((s+k)/2) L(s,χ) be its completed L-function, and let H^χ_t(z) = ∫_0^∞ e^{tu²} Φ_χ(u) cos(zu) du be the de Bruijn–Newman heat flow of Λ(·,χ), normalised so that H^χ_0(z) = (1/8) Λ(1/2 + iz/2, χ). We give a proof, checked by the Lean 4 kernel, that for every such χ and every t ≥ 9/32 all zeros of H^χ_t are real. Equivalently, the generalised de Bruijn–Newman constant satisfies Λ_χ ≤ 9/32. The mathematics is not new, and we say exactly whose it is. De Bruijn's strip-contraction theorem (1950) gives Λ_χ ≤ D²/2 whenever the zeros of H^χ_0 lie in |Im z| ≤ D. Freire, González-Riquelme, Muñoz, Poblete and Salinas observed (arXiv:2610.27343, Remarks 3.1 and 3.4) that the zero-free half-plane Re s > 7/8 for Dirichlet L-functions asserted by OpenAI would give D = 3/4, and hence Λ_χ ≤ 9/32. What this paper adds is a complete formal proof of that composition. For conductors up to 400, FGMPS's unconditional bounds are stronger for 136 of the 242 characters; what is new is that 9/32, for every conductor, is a kernel-checked theorem. OpenAI's half-plane enters as their own kernel-checked Lean theorem. Every other step is proved in Lean on top of Mathlib: de Bruijn's theorem for a general class of kernels, the identification of the theta integral with Mathlib's completed L-function, and Gauss's sign theorem for real primitive characters. The final theorem depends only on the axioms propext, Classical.choice and Quot.sound. In local, unsandboxed replays five checkers accept it: Lean's kernel (run twice), nanoda, and the con-leche/con-ron pair. All five reject a deliberately unsound control. A sandboxed Comparator run against a separately written challenge also accepts it. That run was made by another agent session, and the auditor reproduced its solution export byte for byte. The result rests on OpenAI's Lean proof, whose accompanying manuscript is unrefereed. It is not progress on the Generalised Riemann Hypothesis, which is the statement Λ_χ ≤ 0. A short, separable section records two companion results for ζ that use no OpenAI code, Λ ≤ 225/512 and ψ(x) = x + O_ε(x^{31/32+ε}), both from Cureton and Thorner's half-plane Re s > 31/32. Code, verification records and archive: https://github.com/DrMurphyIsIn/real-dirichlet-dbn-lean (release v1.0.0); DOI 10.5281/zenodo.23840082.

Provenance statement

Text declaration: primarily AI-generated. Human-understanding declaration: some parts of this contribution, but not all, have been checked and understood by a human. How the work was produced. The formalization, the mathematical exposition and the paper's text were developed with extensive assistance from Claude (Anthropic), working as several separate sessions under the author's direction: a drafting session that wrote the paper, an auditing session that reviewed every claim against the Lean sources and its own records, and a runner session that made the sandboxed Comparator runs. The author chose the problem, the venue, the scope and the crediting, decided every question the sessions raised, read Section 2 (the definitions and the formal statement) in full, and approved the release. The paper's Section 8 states how AI was used. What a human has checked and what rests on machines. The author has read and checked the statement layer: the four definitions and the theorem as stated in Lean, and their relation to the classical completed L-function. The proofs have not been checked line by line by a human. They are checked by the Lean 4 kernel and replayed by five independent checkers from three implementation lineages, and a sandboxed Comparator run against a separately written challenge accepted the final theorem. The final theorem depends only on the axioms propext, Classical.choice and Quot.sound. The result rests on OpenAI's kernel-checked Lean proof of a zero-free half-plane, whose accompanying manuscript is unrefereed. Credit. The mathematics is not new: de Bruijn (1950) for the strip-contraction theorem; Freire, Gonzalez-Riquelme, Munoz, Poblete and Salinas (arXiv:2610.27343) for the observation that OpenAI's half-plane gives 9/32; OpenAI for the half-plane; Gauss for the sign theorem; Mathlib for the L-function library. The contribution is the complete, kernel-checked formal proof for every real primitive character. Code and records: https://github.com/DrMurphyIsIn/real-dirichlet-dbn-lean (tag v1.0.0), archived at https://doi.org/10.5281/zenodo.23840082.

Tools used

Anthropic
Claude

References

  1. J. Andrade, A. Chang, and S. J. Miller, Newman's conjecture in various settings , J. Number Theory 144 (2014), 70--91, Cited via FGMPS2026 .
  2. C. Bailey, nanoda_lib : a type checker for L ean 4 export files , https://github.com/ammkrn/nanoda_lib.link
  3. bb (an AI auditor agent session, Claude) , Audit records for the Λχ≤9/32\Lambda_\chi \le 9/32 formalization , Markdown reviews with md5-pinned inputs and outputs; see Appendix A, October 2026, Labelled ``AI review, NOT an operator read-back''. Archived in provenance/ of the release repository.
  4. B. C. Berndt, R. J. Evans, and K. S. Williams, Gauss and J acobi sums , Wiley, New York, 1998, Cited for the history of Gauss's sign theorem; not consulted directly.
  5. H. B ö ving, comparator : a checker for formal challenges , https://github.com/leanprover/comparator, Lean FRO; tag v4.34.0 .link
  6. J. Breitner, K. Morrison, H. B ö ving, et al., lean4export : an exporter for L ean 4 environments , https://github.com/leanprover/lean4export, Version 3.1.0 of the export format.link
  7. M. Carneiro, lean4lean : a L ean 4 kernel written in L ean 4 , https://github.com/digama0/lean4lean.link
  8. D. Cureton and J. Thorner, Report: A quasi- R iemann hypothesis for D edekind zeta functions , Hexagon preprint hexagon:2610.00200v1, October 2026, 12 October 2026. Version 1 states the half-plane Re s>1−1/6000 Re \,s > 1 - 1/6000.hexagon
  9. D. Cureton, J. Thorner, and Axiom Math , DedekindZetaZeroFree : L ean formalization , https://github.com/AxiomMath/DedekindZetaZeroFree, 2026, Commit 09afbb4ce657 . The first public commit 284348a4 states Re s>5999/6000\mathrm{Re}\,s > 5999/6000; commit 201bc40 (13 October 2026) strengthens the theorem main to Re s>31/32\mathrm{Re}\,s > 31/32 for every number field. Lean v4.35.0-rc3 , Mathlib 0493595e . Apache-2.0.link
  10. N. G. de Bruijn, The roots of trigonometric integrals , Duke Math. J. 17 (1950), no. 3, 197--226.
Show all 32 referencesShow fewer references
  1. L. de Moura, Lean now ships with verified kernels , https://leodemoura.github.io/blog/2026-10-15-lean-now-ships-with-verified-kernels/, 2026, 15 October 2026.link
  2. A. Dobner, A proof of N ewman's conjecture for the extended S elberg class , Acta Arith. 201 (2021), no. 1, 29--62.
  3. R. Freire, C. Gonz á lez-Riquelme, C. Mu ñ oz, F. Poblete, and V. Salinas, Upper bounds on the de B ruijn-- N ewman constant for D irichlet LL -functions with primitive real-valued characters , arXiv:2610.27343v1 [math.NT], October 2026, 19 October 2026.arXiv
  4. C. F. Gauss, Summatio quarumdam serierum singularium , Commentationes Societatis Regiae Scientiarum Gottingensis Recentiores 1 (1811).
  5. A. E. Ingham, The distribution of prime numbers , Cambridge Tracts in Mathematics and Mathematical Physics, vol. 30, Cambridge University Press, Cambridge, 1932.
  6. H. Ki, Y.-O. Kim, and J. Lee, On the de B ruijn-- N ewman constant , Adv. Math. 222 (2009), no. 1, 281--306.
  7. Lean FRO , con-leche : an external checker for L ean, proven consistent , https://github.com/leanprover/con-leche, 2026, Implemented and proven consistent by Claude under the supervision of J. Breitner (README).link
  8. — , con-ron : a R ust port of con-leche , https://github.com/leanprover/con-ron, 2026, Written by AI under the supervision of J. Breitner; refinement of con-leche proved with Aeneas (README).link
  9. H. L. Montgomery and R. C. Vaughan, Multiplicative number theory I : Classical theory , Cambridge Studies in Advanced Mathematics, vol. 97, Cambridge University Press, Cambridge, 2006, Cited via FGMPS2026 (Theorems 9.13, 9.16 and 10.8 there).
  10. P. W. Murphy, A kernel-checked bound λ≤9/32\lambda \le 9/32 for the de B ruijn-- N ewman constant from OpenAI 's quasi- R iemann hypothesis , https://github.com/DrMurphyIsIn/qrh-debruijn-newman, 2026, doi:10.5281/zenodo.23269134. The dbn island used here is at commit afd94c7 .DOI
  11. — , Newman's conjecture, kernel-checked: λ≥0\lambda \ge 0 for the de B ruijn-- N ewman constant in L ean 4 along D obner's proof , https://github.com/DrMurphyIsIn/newman-lambda-nonneg, 2026, doi:10.5281/zenodo.23287832 (concept DOI, all versions).DOI
  12. C. M. Newman, Fourier transforms with only real zeros , Proc. Amer. Math. Soc. 61 (1976), no. 2, 245--251.
  13. C. M. Newman and W. Wu, Constants of de B ruijn-- N ewman type in analytic number theory and statistical physics , Bull. Amer. Math. Soc. (N.S.) 57 (2020), no. 4, 595--614, Cited via FGMPS2026 .
  14. OpenAI , The quasi- R iemann hypothesis , OpenAI Math Release preprint OAI:The-Quasi-Riemann-Hypothesis-October-5-2026 , 2026, 5 October 2026; ``written with human assistance''. https://github.com/openai/math/blob/main/preprints/The-Quasi-Riemann-Hypothesis-October-5-2026/paper2.pdf.link
  15. — , The quasi- R iemann hypothesis: A zero-free half-plane Re(s)>7/8\mathrm{Re}(s)>7/8 , OpenAI Math Release preprint OAI:The-Quasi-Riemann-Hypothesis-September-30-2026 , 2026, 30 September 2026. https://github.com/openai/math/blob/main/preprints/The-Quasi-Riemann-Hypothesis-September-30-2026/paper.pdf.link
  16. — , openai/math : L ean library accompanying the OpenAI math release , https://github.com/openai/math, 2026, Commit adc7f1241b42e322a6451854ab7e4b4c146bf78a ; Lean v4.34.1 , Mathlib d13f23b . Theorem OAI.DirichletCharacter.LFunction_ne_zero_of_seven_eighths_lt_re , file lean/OAI/NumberTheory/DirichletL/Nonvanishing.lean ; challenge lean/ComparatorChallenges/DirichletSevenEighths.lean . Apache-2.0.link
  17. D. Platt and T. Trudgian, The R iemann hypothesis is true up to 310123 10^ 12 , Bull. London Math. Soc. 53 (2021), no. 3, 792--797.
  18. D. J. Platt, Numerical computations concerning the GRH , Math. Comp. 85 (2016), no. 302, 3009--3027, Cited via FGMPS2026 .
  19. D. H. J. Polymath, Effective approximation of heat flow evolution of the R iemann ξ\xi function, and a new upper bound for the de B ruijn-- N ewman constant , Res. Math. Sci. 6 (2019), Paper 31, arXiv:1904.12438.arXiv
  20. B. Rodgers and T. Tao, The de B ruijn-- N ewman constant is non-negative , Forum Math. Pi 8 (2020), e6, arXiv:1801.05914.arXiv
  21. J. Stopple, Notes on low discriminants and the generalized N ewman conjecture , Funct. Approx. Comment. Math. 51 (2014), no. 1, 23--41, Cited via FGMPS2026 .
  22. The mathlib Community , The L ean mathematical library , Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP 2020), ACM, 2020, Revisions used here: 0493595e and d13f23b , pp. 367--381.

Version history

  1. v1Submitted by Peter W. Murphy, MDInitial depositCurrentOct 31, 2026