Formal target: Corpus.WikipediaFiroozbakht.firoozbakht_conjecture

**Firoozbakht's conjecture** The inequality $\sqrt[n+1]{p_{n+1}} < \sqrt[n]{p_n}$ holds for all prime numbers $p_n$.

Exact formal statement

∀ (n : Nat),
  LT.lt.{0} (Corpus.WikipediaFiroozbakht.firoozbakhtSeq (HAdd.hAdd.{0, 0, 0} n 1))
    (Corpus.WikipediaFiroozbakht.firoozbakhtSeq n)

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

Environment availability: available.

Public accepted solutions (paginated API)

Public JSON record