Formal target: Corpus.Erdos913.erdos_913.variants.infinite_many_8p_sq_add_one_primes

It is likely that there are infinitely many primes $p$ such that $8p^2 - 1$ is also prime.

Exact formal statement

Set.Infinite.{0}
  (Set.ofPred.{0} fun p =>
    And (Nat.Prime p) (Nat.Prime (HSub.hSub.{0, 0, 0} (HMul.hMul.{0, 0, 0} 8 (HPow.hPow.{0, 0, 0} p 2)) 1)))

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

Environment availability: available.

Public accepted solutions (paginated API)

Public JSON record