Oppermann's Conjecture

Exact formalization occurrence from the upstream source collection.

Tracked question

For every integer

x \ge 2

, the following hold: - There exists a prime between

x(x-1)

and

x^2

. - There exists a prime between

x^2

and

x(x+1)

Lean declaration

theorem oppermann_conjecture (x : ℕ) (hx : 2 ≤ x) :
    (∃ p ∈ Ioo (x * (x - 1)) (x^2), p.Prime) ∧
    (∃ p ∈ Ioo (x^2) (x * (x + 1)), p.Prime)