Formal target: Corpus.Erdos779.erdos_779

A Conjecture of Marian Deaconescu, see p.120 in https://doi.org/10.2307/2975810 [Needed to index shift in order to avoid trivial case $n = 0$, where the conjecture is trivially false.]

Exact formal statement

∀ (n : Nat),
  GE.ge.{0} n 1 →
    have P := Finset.prod.{0, 0} (Finset.range (HAdd.hAdd.{0, 0, 0} n 1)) fun i => Nat.nth Nat.Prime i;
    Exists.{1} fun p =>
      And (Nat.Prime p)
        (And (Nat.Prime (HAdd.hAdd.{0, 0, 0} P p)) (And (LT.lt.{0} (Nat.nth Nat.Prime n) p) (LT.lt.{0} p P)))

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

Environment availability: available.

Public accepted solutions (paginated API)

Public JSON record