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

Abstract

This note gives Lean proofs, with no hypothesis, of the primality criterion of Saouter's paper, Lemma 1 for every even F, 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*10^18 as an explicit hypothesis, a ladder of 25 Proth primes reaches 10^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. Lean source: github.com/sthubbar/goldbach-lean, entries/saouter1998, commit 39d1ce6; registered in the Palomar registry as PALOMAR-2026-11-02-000012.

Keywords