Fibonacci Primes

Reference: Wikipedia

theorem FibonacciPrimes.fib_primes_infinite : {n : ℕ | (∃ (m : ℕ), Nat.fib m = n) ∧ Nat.Prime n}.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).

theorem FibonacciPrimes.fib_primes_infinite.variant : {n : ℕ | Nat.Prime (Nat.fib n)}.Infinite

There are infinitely many indices $i$, such that the $i$-th Fibonacci is prime.

theorem FibonacciPrimes.indices_infinite_iff_fib_primes_infinite : {n : ℕ | Nat.Prime (Nat.fib n)}.Infinite ↔ {n : ℕ | (∃ (m : ℕ), Nat.fib m = n) ∧ Nat.Prime n}.Infinite

The two ways of phrasing the conjecture are equivalent.