Formal target: Corpus.WikipediaOppermann.oppermann_conjecture.parts.i

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

Exact formal statement

∀ (x : Nat),
  LE.le.{0} 2 x →
    Exists.{1} fun p =>
      And
        (Membership.mem.{0, 0}
          (Finset.Ioo.{0} (HMul.hMul.{0, 0, 0} x (HSub.hSub.{0, 0, 0} x 1)) (HPow.hPow.{0, 0, 0} x 2)) p)
        (Nat.Prime p)

This target is a formal statement, not a proof of the problem.

Environment availability: available.

Public accepted solutions (paginated API)

Public JSON record