Formal target: Corpus.OEIS1359.conjecture

Primes $p_k$ such that $p_k!

Exact formal statement

∀ (k : Nat),
  GT.gt.{0} k 1 →
    have Pk := Nat.nth Nat.Prime (HSub.hSub.{0, 0, 0} k 1);
    have Pk_succ := Nat.nth Nat.Prime k;
    have Congruence := Pk_succ.ModEq Pk.factorial 1;
    have IsLesserTwinPrime := Nat.Prime (HAdd.hAdd.{0, 0, 0} Pk 2);
    have Wk_prod :=
      Finset.prod.{0, 0} (Finset.Icc.{0} (HAdd.hAdd.{0, 0, 0} Pk 1) (HSub.hSub.{0, 0, 0} Pk_succ 2)) fun i => i;
    Iff Congruence
      (Or IsLesserTwinPrime
        (Or (Eq.{1} k 991) (And (GT.gt.{0} (HSub.hSub.{0, 0, 0} Pk_succ Pk) 2) (Pk_succ.ModEq Wk_prod 1))))

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

Environment availability: available.

Public accepted solutions (paginated API)

Public JSON record