HEXAGONbeta

Saouter's primality criterion in Lean, a ladder constant, and a 25 rung route to odd Goldbach up to 102010^{20}

Primarily AI-generated textHuman understanding: some partsmath.NT — Number Theory

Contributed by Steve Hubbard ↗

Version 1 / Nov 06, 2026 / CC BY 4.0

Abstract

This note gives Lean proofs, with no hypothesis, of the primality criterion of Saouter's paper, Lemma 1 for every even FF, Theorems 1 and 2, and it records the reading of the constant on page 865 under which the formula agrees with the rest of the paper; separately, given the published even Goldbach computation to 4⋅10184\cdot 10^{18} as an explicit hypothesis, a ladder of 25 Proth primes reaches 102010^{20} in the Lean kernel. The binary Goldbach conjecture remains open and this note makes no progress on it. The ternary Goldbach theorem for all odd numbers is Helfgott's (arXiv:1312.7748), and it is not formalized here and not used.

Author comments: 8 pages. Version 3 of the note, first deposit on Hexagon.

Provenance statement

Steve Hubbard designed the research program and directed this work. AI tools, Claude, Codex, Gemini and Antigravity, wrote the Lean code and drafted the text, and AI agents did the checks of the Lean against the source. No human expert has reviewed the mathematics. The Lean source is public at github.com/sthubbar/goldbach-lean at commit 39d1ce6, and the entry is registered in the Palomar registry as PALOMAR-2026-11-02-000012. Agent session logs are not attached, since they hold private email. Also posted as aiXiv:2611.00468 and aixiv.261105.000001 v1.0.

References

  1. J. Brillhart, D. H. Lehmer, and J. L. Selfridge, New primality criteria and factorizations of 2m±12^m \pm 1 , Math. Comp. 29 (1975), no. 130, 620--647.
  2. H. A. Helfgott, The ternary Goldbach conjecture is true , arXiv:1312.7748 , 2013.arXiv
  3. H. A. Helfgott and D. J. Platt, Numerical verification of the ternary Goldbach conjecture up to 8.875⋅10308.875\cdot 10^{30} , Exp. Math. 22 (2013), 406--409.
  4. T. Oliveira e Silva, S. Herzog, and S. Pardi, Empirical verification of the even Goldbach conjecture and computation of prime gaps up to 4⋅10184\cdot 10^{18} , Math. Comp. 83 (2014), no. 288, 2033--2060.
  5. O. Ramaré and Y. Saouter, Short effective intervals containing primes , J. Number Theory 98 (2003), 10--33.
  6. Y. Saouter, Checking the odd Goldbach conjecture up to 102010^{20} , Math. Comp. 67 (1998), no. 222, 863--866, doi:10.1090/S0025-5718-98-00928-4 .DOI
  7. M. K. Sinisalo, Checking the Goldbach conjecture up to 4⋅10114\cdot 10^{11} , Math. Comp. 61 (1993), no. 204, 931--934.

Version history

  1. v1 · 8 pagesSubmitted by Steve Hubbard8 pages. Version 3 of the note, first deposit on Hexagon.CurrentNov 06, 2026