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