Independent reproduction of OpenAI's Lean proof: ζ(s) has no zeros for Re(s) > 7/8

Researchers independently reproduced OpenAI's Lean proof generated by an AI model and concluded that the proof passes inspection. The proof claims that the Riemann zeta function has no zeros for Re(s) > 7/8, a step forward from earlier results that only excluded Re(s)=1 and a very narrow region to its left, but it does not amount to a proof of the Riemann hypothesis. The proof comprises about 2,900 files and nearly 500,000 lines; both Lean's built-in kernel and a separate Rust-based independent implementation, the nanoda kernel, accept the proof, which relies on only three standard axioms of Lean. The reproducers noted several uncovered aspects: both checks were performed by the same operator on the same machine, and no one has yet independently reproduced it from a fresh clone; the check assumes the OpenAI repository is non-adversarial, and its build configuration and 23 dependency patches run outside the comparator sandbox during the setup phase; OpenAI's configuration disables the second kernel by default (402 of 405 set to false), and this reproduction turned it on.