45. RH to height 50, then 100, kernel-checked

On 2026-10-22 this laboratory finished a Lean proof, about Mathlib's own riemannZeta, that every nontrivial zero up to height 50 lies on the critical line and is simple, and that there are exactly ten of them. It is a theorem, in the sense this repository reserves for the word: Lean's kernel accepts it with zero sorry and only the three standard axioms. This page leads with it and carries forward the results of docs/39. On 2026-10-23 a clean Lean source build also closed height 100: 29 distinct zeros in the open critical strip, all on the line and simple. Independent whole-closure replay was accepted by con-ron --verified on 2026-10-24.

The theorems are finite. The height-100 result says nothing above 100 or about the Riemann hypothesis (docs/08). Numerical verification of RH reaches far higher, to 3 * 10^12; the distinction here is a Lean-kernel-checked theorem with no outside computation assumed as an axiom. A bounded search on 2026-10-22 found Lean statements of RH to a height that rest on external computations as axioms, and found no earlier standard-axiom formal proof. That search does not establish priority. The rows carried from docs/39 keep their own grades: they are conditional on OpenAI's theorem and unreviewed by any person.

The results

RH to height 100

Riemann's hypothesis says every nontrivial zero of zeta has real part 1/2. Computers have checked trillions of zeros, including rigorous interval-arithmetic work, but that is distinct from a formal kernel proof. Hunt #137 first proved height 50 (ten zeros) and then height 100 (29 distinct zeros) in Lean. The route counts every zero in the strip with the argument principle, encloses the Gamma-side term with a Stirling bound and the zeta side with interval boxes the kernel decides, and matches the count against ten zeros already located on the line by sign changes of Hardy's Z (hunts #132 and #133), plus nineteen further zeros in generated boxes. The count on 3 < Im rho <= 100 lies strictly between 28 and 30, hence equals 29; the low-height lemma excludes zeros with 0 < Im rho <= 3. Because the upper count matches all 29 located zeros, no off-line or multiple zero hides in the open strip at positive ordinate through the inclusive upper endpoint 100. The height-50 theorem is below the Davenport-Heilbronn function's first off-line zero at height 85.699; height 100 crosses it, but neither finite result proves RH.

OUT=/path/to/fresh-output
LEAN="$(cd lean && elan which lean)" LAKE_DIR="$PWD/lean/.lake" \
  bash hunts/rh_height_lean/lean/build.sh --full100 "$OUT" > "$OUT.build.log" 2>&1
.venv/bin/python hunts/rh_height_lean/lean/check_axioms.py "$OUT.build.log" --full100
.venv/bin/python -m pytest -q hunts/rh_height_lean

Use the root package's pinned Lean v4.35.0-rc2 and Mathlib 065356127b1dc0016f66b7283ce0ce2c4055aa55 dependency objects. The clean build of 2026-10-23 exited 0, and the final axiom audit accepted all 100 reports with only propext, Classical.choice and Quot.sound. On 2026-10-24 the independent checker con-ron --verified accepted the exported closure of the three final theorems: 82,680 declarations accepted, 81,674 of 81,674 checks done, exit 0. Earlier runs of con-ron, NanoDa and leanchecker --fresh stopped at time or memory bounds without a verdict; none rejected the proof. On 2026-10-26, rerun with no wall bound, leanchecker --fresh replayed the whole closure through Lean's own kernel from an empty environment and exited 0 after 1 h 40 min. That is a same-kernel replay, not an independent checker. NanoDa stopped again at the free-memory floor without a verdict. Commands, hashes and every attempt are in hunt #137's RESULTS. This is acceptance by two proof checkers, not review by a person.

The earlier results

Carried from docs/39, which has the full account of each and the grades above. The openings below are quoted from it.

The input

OpenAI, "The Quasi-Riemann Hypothesis", OpenAI Math Release preprint dated 30 September 2026, Theorem 1.1: every finite-order Hecke L-function over Q(sqrt(-3)), hence every Dirichlet L-function and zeta itself, has no zero in Re s > 7/8. A companion dated 5 October 2026, written with human assistance, proves the weaker half-plane Re s > 11/12 by part of the same method.

Class numbers up to 1500

The class number h(D) of an imaginary quadratic field counts how far unique factorisation fails in its ring of integers. Gauss asked which fields have class number 1; the answer (nine fields) took until Heegner, Baker and Stark, and Watkins completed every h <= 100 in 2004. The difficulty is always the same: a lower bound h(D) >= f(D) that is explicit, so that only finitely many D can have a given class number and one can search them all.

A prime between consecutive ninth powers

Legendre's conjecture asks for a prime between consecutive squares, and it is open. For a k-th power version valid for every n, the best unconditional k was 86 as of 2026. Given the 7/8 half-plane the explicit formula for primes has an error of size x^(7/8) (log x)^2, which beats the gap (n+1)^k - n^k, about k x^(1 - 1/k), exactly when k >= 9. The hunt closes k = 9 for every n: an exact explicit formula for a smooth weight, sums over zeros bounded in closed form from explicit zero counts, an Arb cover of 10 <= n <= e^100, an analytic tail, and Pratt certificates for n <= 9. It closes even if no zero is assumed to lie on the critical line; the published verification of RH up to height 3 * 10^12 only widens the margins. OpenAI's weaker 11/12 half-plane alone gives k = 13. With the same method and no further input k = 8 fails, so 9 is the floor of the half-plane alone. The hunt's doors named the way below it: an explicit zero-density estimate, which thins out the zeros near real part 7/8. The next section takes that door.

A prime between consecutive seventh powers

The October 8 extensions (hunts/oct08_extensions/, PR #282) keep hunt #126's weight, explicit formula and tail routine and add one published input: Kadiri, Lumley and Ng's explicit zero-density estimate (arXiv:2101.12263v1, Lemma 4.14 and Table 1), which bounds how many zeros have real part above sigma at five values of sigma from 3/4 to 0.87. A single split at 0.85 already closes k = 8. Splitting the zeros between 3/4 and 7/8 into all five strips, each counted with a positive coefficient so that no two independently bounded counts are ever subtracted, closes k = 7: for every integer n >= 1 there is a prime strictly between n^7 and (n+1)^7, given the half-plane and that estimate. The finite part is a cover of 2.25 <= log n <= 50 by 764 Arb cells, every margin above 0.13045, an analytic tail below 0.012961 beyond it, and trial-division witnesses for n <= 9; the replay asserts each of those inequalities and tests/test_seventh_power_replay.py runs it. The same bound fails at k = 6 near log n = 29: a failure of this bound, not a statement about primes.

Small witnesses

If chi is a character mod q that is not identically 1 on the units, how far must one search to find an n with chi(n) != 1? Under GRH the answer is about (log q)^2 (Ankeny, Bach). With a zero-free half-plane Re s > theta the classical exponent is 1/(1 - theta), which is 8 here. The hunt proves it with constant 1: n <= (log q)^8 for every q >= 3, tight at q = 3, and (0.7 log q)^8 for q >= 5. The sum over zeros is priced exactly by Hadamard's identity, with no zero counting at all. Consequences: the least quadratic nonresidue mod p is at most (log p)^8; every odd composite n has a Miller-Rabin witness at most (0.7 log n)^8, so Miller's deterministic primality test runs with an explicit witness range; and the units mod q are generated by the primes up to (log q)^8. The exponent 8 is not new as a conditional statement (Rodosskii; Montgomery and Vaughan, Theorem 13.12); the explicit constant and the all-moduli statement were not found in the search. The least primitive root was also attempted: the bound obtained is smaller than any power of p but not a power of log p.

Linnik's constant

Linnik proved that every reduced class mod q contains a prime below q^L for some fixed L; the best unconditional L is 5. Under GRH it is 2. With every zero at real part at most 7/8, the Siegel zero, the Deuring-Heilbronn repulsion and the log-free density estimates all drop out of the argument, and L is governed by the zero-density exponent for the family of characters mod q on 1/2 <= sigma <= 7/8. With Chen, Gupta and Li's 2025 density estimate this gives L <= 7/3; with refereed inputs alone, 12/5. Chen, Gupta and Li already state the conditional implication without proof, so this is the unconditional instantiation and a complete written proof rather than a new idea. Corollaries: the expected count of primes in every class once x >= q^(7/3 + eps), and a prime in almost every class below q^(7/6 + eps).

Related: docs/39, hunt #137, hunts/README.md.