Fibonacci Primes

Conjectura.Problems.WP0013.Statement

/-
Copyright (c) 2025 The Formal Conjectures Authors. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: The Formal Conjectures Authors
-/
import Mathlib

/-! # Fibonacci Primes

## Source

Adapted for Conjectura from [formal-conjectures](https://github.com/google-deepmind/formal-conjectures) (Google DeepMind), `Wikipedia/FibonacciPrimes.lean`. The problem is catalogued at [https://en.wikipedia.org/wiki/Fibonacci_prime](https://en.wikipedia.org/wiki/Fibonacci_prime).

LOCKED: solvers cannot modify this file.
-/

namespace Conjectura.WP0013

/--
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 fib_primes_infinite : {n : ℕ | (∃ m : ℕ, m.fib = n) ∧ n.Prime}.Infinite := by
  sorry

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

theorem fib_primes_infinite.variant : {n : ℕ | n.fib.Prime}.Infinite := by
  sorry

/--
The two ways of phrasing the conjecture are equivalent.
-/

theorem indices_infinite_iff_fib_primes_infinite : type_of% fib_primes_infinite.variant ↔
    type_of% fib_primes_infinite := by
  simp only [Set.infinite_iff_exists_gt]
  constructor
  · intros h a
    rcases h (a + 1) with ⟨b', ⟨hb₁, hb₂⟩⟩
    use Nat.fib b'
    exact ⟨⟨exists_apply_eq_apply Nat.fib b', hb₁⟩,
      by linear_combination b'.le_fib_add_one + hb₂⟩
  · intro h a
    rcases h (Nat.fib a) with ⟨b', ⟨⟨m, hm⟩, hb₁⟩, hb₂⟩
    use m
    constructor
    · simp_all
    · have := @m.fib_mono a
      omega

/-- 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). -/
def goal : Prop :=
  {n : ℕ | (∃ m : ℕ, m.fib = n) ∧ n.Prime}.Infinite

end Conjectura.WP0013