Skip to content

Formal ConjecturesWikipedia

For every integer x≥2x \ge 2 there exists a prime between x(x−1)x(x-1) and x2x^2.

Exact formalization occurrence from the upstream source collection.

Open source
Source category
research open
Formal proof
Not retained
Vela current state
No Repository Result attached

Lean declaration

Open source view
theorem oppermann_conjecture.parts.i (x : ℕ) (hx : 2 ≤ x) :
    ∃ p ∈ Ioo (x * (x - 1)) (x^2), p.Prime

Related formalizations

Search problems.science

Find a Problem, Result, source, or page