Formal target: Corpus.OEIS55487.conjecture

Conjecture: unless $n!

Exact formal statement

∀ (n : Nat),
  LE.le.{0} 1 n →
    Not (Corpus.OEIS55487.isFactorialPrime n) →
      Ne.{1} (Corpus.OEIS55487.a n) 0 →
        Nat.Prime (Corpus.OEIS55487.p n) →
          Eq.{1} (Corpus.OEIS55487.a n) (HMul.hMul.{0, 0, 0} (Corpus.OEIS55487.p n) (Corpus.OEIS55487.q n))

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

Environment availability: available.

Public accepted solutions (paginated API)

Public JSON record