Formal target: Corpus.WikipediaPierpontPrime.infinitely_many_pierpont_primes
There are infinitely many Pierpont primes.
Exact formal statement
Set.Infinite.{0} (Set.ofPred.{0} fun p => Corpus.WikipediaPierpontPrime.IsPierpontPrime p)This target is a formal statement, not a proof of the problem.
Environment availability: available.