Formal target: Corpus.OEIS135508.conjecture

Conjecture: For prime $p$ such that $p-2$ is not a prime, $a(p-1) = p$.

Exact formal statement

∀ (p : Nat),
  Nat.Prime p → Not (Nat.Prime (HSub.hSub.{0, 0, 0} p 2)) → Eq.{1} (Corpus.OEIS135508.a (HSub.hSub.{0, 0, 0} p 1)) p

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

Environment availability: available.