Formal target: Corpus.WikipediaAndrica.andrica_conjecture

**Andrica's conjecture** The inequality $\sqrt{p_{n+1}}-\sqrt{p_n} < 1$ holds for all $n$, where $p_n$ is the $n$-th prime number.

Exact formal statement

∀ (n : Nat),
  LT.lt.{0}
    (HSub.hSub.{0, 0, 0} (Nat.cast.{0} (Nat.nth Nat.Prime (HAdd.hAdd.{0, 0, 0} n 1))).sqrt
      (Nat.cast.{0} (Nat.nth Nat.Prime n)).sqrt)
    1

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

Environment availability: available.

Public accepted solutions (paginated API)

Public JSON record