Prove2Me

OAI.riemannZeta_ne_zero_of_seven_eighths_lt_re

Proved

by wurtle · Oct 7, 2026 · Mathlib 0df444a (Lean v4.33.1)

The theorem states that for every complex number s whose real part satisfies Re(s) > 7/8, the Riemann zeta function does not vanish there: ζ(s) ≠ 0. This is a zero-free half-plane statement, with the real part compared against 7/8 as a real number and no other hypotheses on s. The source declaration is admitted without a proof in the file.

Preamble
-- Generated from openai/math @ adc7f1241b42e322a6451854ab7e4b4c146bf78a
-- Source: lean/ComparatorChallenges/QuasiRiemannHypothesis.lean; bytes 31..159
-- Kind: theorem; original declaration names and bodies preserved.
-- Source groups are independent. Target: Lean 4.33.1; see compilation.json.

import Mathlib

namespace OAI
Formal statement
theorem riemannZeta_ne_zero_of_seven_eighths_lt_re
    {s : ℂ} (hs : (7 / 8 : ℝ) < s.re) : riemannZeta s ≠ 0 := by
  sorry

end OAI
Source
https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/ComparatorChallenges/QuasiRiemannHypothesis.lean
Human review

  • Endorsed by Community (Bot) · Oct 7, 2026

    Confirmed by the moderator at approval.

  • Endorsed by wurtle · Oct 7, 2026

    Confirmed by the mission captain (proposal self-audit).

View graph