FormalConjectures.Wikipedia.FibonacciPrimes

/-
Copyright 2025 The Formal Conjectures Authors.

Licensed under the Apache License, Version 2.0 (the "License");
you may not use this file except in compliance with the License.
You may obtain a copy of the License at

    https://www.apache.org/licenses/LICENSE-2.0

Unless required by applicable law or agreed to in writing, software
distributed under the License is distributed on an "AS IS" BASIS,
WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
See the License for the specific language governing permissions and
limitations under the License.
-/

import FormalConjecturesUtil

Fibonacci Primes

Reference: Wikipedia


namespace FibonacciPrimes

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).

@[category research open, AMS 11]
theorem declaration uses 'sorry'fib_primes_infinite : {n : ℕ | (∃ m : ℕ, m.fib = n) ∧ n.Prime}.Infinite := by⊢ {n | (∃ m, Nat.fib m = n) ∧ Nat.Prime n}.Infinite
  sorryAll goals completed! 🐙

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

@[category research open, AMS 11]
theorem declaration uses 'sorry'fib_primes_infinite.variant : {n : ℕ | n.fib.Prime}.Infinite := by⊢ {n | Nat.Prime (Nat.fib n)}.Infinite
  sorryAll goals completed! 🐙

The two ways of phrasing the conjecture are equivalent.

@[category test, AMS 11]
theorem indices_infinite_iff_fib_primes_infinite : type_of% fib_primes_infinite.variant ↔
    type_of% fib_primes_infinite := by⊢ {n | Nat.Prime (Nat.fib n)}.Infinite ↔ {n | (∃ m, Nat.fib m = n) ∧ Nat.Prime n}.Infinite
  simp only [Set.infinite_iff_exists_gt]⊢ (∀ (a : ℕ), ∃ b ∈ {n | Nat.Prime (Nat.fib n)}, a < b) ↔ ∀ (a : ℕ), ∃ b ∈ {n | (∃ m, Nat.fib m = n) ∧ Nat.Prime n}, a < b
  constructormp⊢ (∀ (a : ℕ), ∃ b ∈ {n | Nat.Prime (Nat.fib n)}, a < b) → ∀ (a : ℕ), ∃ b ∈ {n | (∃ m, Nat.fib m = n) ∧ Nat.Prime n}, a < bmpr⊢ (∀ (a : ℕ), ∃ b ∈ {n | (∃ m, Nat.fib m = n) ∧ Nat.Prime n}, a < b) → ∀ (a : ℕ), ∃ b ∈ {n | Nat.Prime (Nat.fib n)}, a < b
  ·mp⊢ (∀ (a : ℕ), ∃ b ∈ {n | Nat.Prime (Nat.fib n)}, a < b) → ∀ (a : ℕ), ∃ b ∈ {n | (∃ m, Nat.fib m = n) ∧ Nat.Prime n}, a < b intros h amph:∀ (a : ℕ), ∃ b ∈ {n | Nat.Prime (Nat.fib n)}, a < ba:ℕ⊢ ∃ b ∈ {n | (∃ m, Nat.fib m = n) ∧ Nat.Prime n}, a < b
    rcases h (a + 1) with ⟨b', ⟨hb₁, hb₂⟩⟩mph:∀ (a : ℕ), ∃ b ∈ {n | Nat.Prime (Nat.fib n)}, a < ba:ℕb':ℕhb₁:b' ∈ {n | Nat.Prime (Nat.fib n)}hb₂:a + 1 < b'⊢ ∃ b ∈ {n | (∃ m, Nat.fib m = n) ∧ Nat.Prime n}, a < b
    use Nat.fib b'hh:∀ (a : ℕ), ∃ b ∈ {n | Nat.Prime (Nat.fib n)}, a < ba:ℕb':ℕhb₁:b' ∈ {n | Nat.Prime (Nat.fib n)}hb₂:a + 1 < b'⊢ Nat.fib b' ∈ {n | (∃ m, Nat.fib m = n) ∧ Nat.Prime n} ∧ a < Nat.fib b'
    exact ⟨⟨exists_apply_eq_apply Nat.fib b', hb₁⟩,
      byh:∀ (a : ℕ), ∃ b ∈ {n | Nat.Prime (Nat.fib n)}, a < ba:ℕb':ℕhb₁:b' ∈ {n | Nat.Prime (Nat.fib n)}hb₂:a + 1 < b'⊢ a < Nat.fib b' linear_combination b'.le_fib_add_one + hb₂All goals completed! 🐙⟩
  ·mpr⊢ (∀ (a : ℕ), ∃ b ∈ {n | (∃ m, Nat.fib m = n) ∧ Nat.Prime n}, a < b) → ∀ (a : ℕ), ∃ b ∈ {n | Nat.Prime (Nat.fib n)}, a < b intro h amprh:∀ (a : ℕ), ∃ b ∈ {n | (∃ m, Nat.fib m = n) ∧ Nat.Prime n}, a < ba:ℕ⊢ ∃ b ∈ {n | Nat.Prime (Nat.fib n)}, a < b
    rcases h (Nat.fib a) with ⟨b', ⟨⟨m, hm⟩, hb₁⟩, hb₂⟩mprh:∀ (a : ℕ), ∃ b ∈ {n | (∃ m, Nat.fib m = n) ∧ Nat.Prime n}, a < ba:ℕb':ℕhb₂:Nat.fib a < b'hb₁:Nat.Prime b'm:ℕhm:Nat.fib m = b'⊢ ∃ b ∈ {n | Nat.Prime (Nat.fib n)}, a < b
    use mhh:∀ (a : ℕ), ∃ b ∈ {n | (∃ m, Nat.fib m = n) ∧ Nat.Prime n}, a < ba:ℕb':ℕhb₂:Nat.fib a < b'hb₁:Nat.Prime b'm:ℕhm:Nat.fib m = b'⊢ m ∈ {n | Nat.Prime (Nat.fib n)} ∧ a < m
    constructorh.lefth:∀ (a : ℕ), ∃ b ∈ {n | (∃ m, Nat.fib m = n) ∧ Nat.Prime n}, a < ba:ℕb':ℕhb₂:Nat.fib a < b'hb₁:Nat.Prime b'm:ℕhm:Nat.fib m = b'⊢ m ∈ {n | Nat.Prime (Nat.fib n)}h.righth:∀ (a : ℕ), ∃ b ∈ {n | (∃ m, Nat.fib m = n) ∧ Nat.Prime n}, a < ba:ℕb':ℕhb₂:Nat.fib a < b'hb₁:Nat.Prime b'm:ℕhm:Nat.fib m = b'⊢ a < m
    ·h.lefth:∀ (a : ℕ), ∃ b ∈ {n | (∃ m, Nat.fib m = n) ∧ Nat.Prime n}, a < ba:ℕb':ℕhb₂:Nat.fib a < b'hb₁:Nat.Prime b'm:ℕhm:Nat.fib m = b'⊢ m ∈ {n | Nat.Prime (Nat.fib n)} simp_allAll goals completed! 🐙
    ·h.righth:∀ (a : ℕ), ∃ b ∈ {n | (∃ m, Nat.fib m = n) ∧ Nat.Prime n}, a < ba:ℕb':ℕhb₂:Nat.fib a < b'hb₁:Nat.Prime b'm:ℕhm:Nat.fib m = b'⊢ a < m have := @m.fib_mono ah.righth:∀ (a : ℕ), ∃ b ∈ {n | (∃ m, Nat.fib m = n) ∧ Nat.Prime n}, a < ba:ℕb':ℕhb₂:Nat.fib a < b'hb₁:Nat.Prime b'm:ℕhm:Nat.fib m = b'this:m ≤ a → Nat.fib m ≤ Nat.fib a := Nat.fib_mono⊢ a < m
      omegaAll goals completed! 🐙


end FibonacciPrimes