Independent re-run of the Lean check for OpenAI's ζ(s) ≠ 0 for Re(s) > 7/8 proof: "the proof checks"

Repository created 01:36 UTC Oct 7 (posted to HN as "Verified Riemann Zeta in Lean"). It re-runs the Lean check of OAI.riemannZeta_ne_zero_of_seven_eighths_lt_re from openai/math at commit adc7f12 (Lean/Mathlib v4.34.1). Lean FRO's comparator with OpenAI's challenge, and with a challenge written independently for the check plus the independent nanoda kernel (Rust), both accept. The only axioms are propext, Classical.choice and Quot.sound, and the statement uses Mathlib's own riemannZeta. The proof is about 2,900 files and close to half a million lines. Caveats from the README: one operator on one machine, OpenAI's repository assumed non-adversarial, and the written paper was not reviewed. Goldblatt's X bio links him to Meta and two start-ups; he is not identified as a mathematician.

(pending: to be filled by npm run fetch-posts; views quoted above are from fxtwitter on 2026-10-07 around 05:20 UTC)