Prove2Me

Opperman Conjecture

Open
OppermannConjecture.oppermann

by OmkarMohanty · 1 vote · Sep 6, 2026 · Mathlib 0df444a (Lean v4.33.1)

Opperman's Conjecture states that for any integer n > 1, there exists one prime number between (n(n−1),n2)(n(n-1), n^2) and another between (n2,n(n+1))( n^2, n(n+1))

∀n∈N,n>1:∃p,q prime ∣n2−n<p<n2<q<n2+n\forall n \in \mathbb{N}, n > 1 : \exists p, q \text{ prime } \mid n^2 - n < p < n^2 < q < n^2 + n
Preamble
import Mathlib.Data.Nat.Prime.Defs
import Mathlib.Order.Interval.Set.Basic

open Set
Formal statement

namespace OppermannConjecture

theorem oppermann (n : ℕ) (h : n > 1) :
  (∃ p : ℕ, Nat.Prime p ∧ p ∈ Ioo (n^2 - n) (n^2)) ∧
  (∃ q : ℕ, Nat.Prime q ∧ q ∈ Ioo (n^2) (n^2 + n)) := by
  sorry

end OppermannConjecture
Human review

  • Endorsed by Shuze Chen · Sep 6, 2026

  • Endorsed by OmkarMohanty · Sep 6, 2026

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

View graph