Formal target: Corpus.WikipediaFibonacciPrimes.fib_primes_infinite
There are infinitely many Fibonacci primes, i.e., Fibonacci numbers that are prime It is also a barrier to defining a benchmark from this paper: https://arxiv.org/html/2505.13938v1 (see Figure 8).
Exact formal statement
Set.Infinite.{0} (Set.ofPred.{0} fun n => And (Exists.{1} fun m => Eq.{1} (Nat.fib m) n) (Nat.Prime n))This target is a formal statement, not a proof of the problem.
Environment availability: available.