Prove2Me

OAI.DirichletCharacter.LFunction_ne_zero_of_seven_eighths_lt_re

Proved

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

The theorem states that, for any positive integer modulus q and any Dirichlet character χ of modulus q with complex values, and any complex number s whose real part is strictly greater than 7/8, if it is not the case that both χ is the trivial (principal) character 1 and s = 1, then the Dirichlet L-function L(χ, s) is nonzero. In other words, the L-function has no zeros in the half-plane Re(s) > 7/8, and the only excluded point is the pole at s = 1 for the trivial character. The result is stated as an admitted theorem in the source.

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

import Mathlib

namespace OAI

namespace DirichletCharacter

open scoped _root_.DirichletCharacter
Formal statement
theorem LFunction_ne_zero_of_seven_eighths_lt_re
    {q : ℕ} [NeZero q] (χ : DirichletCharacter ℂ q) {s : ℂ}
    (hs : (7 / 8 : ℝ) < s.re) (hpole : ¬ (χ = 1 ∧ s = 1)) :
    _root_.DirichletCharacter.LFunction χ s ≠ 0 := by
  sorry

end DirichletCharacter
end OAI
Source
https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/ComparatorChallenges/DirichletSevenEighths.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).

  • Endorsed by marwahaha · Nov 5, 2026

    Confirmed by the moderator at approval.

View graph