Fibonacci Primes
fib_primes_infinitetheorem
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
sorryvarianttheorem
There are infinitely many indices , such that the -th Fibonacci is prime.
theorem fib_primes_infinite.variant : {n : ℕ | n.fib.Prime}.Infinite := by
sorryindices_infinite_iff_fib_primes_infinitetheorem
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
omegagoaldef
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}.Infiniteimport Conjectura.Problems.WP0013.Statement · maintainer — open · raw source
Adapted for Conjectura from formal-conjectures (Google DeepMind), `Wikipedia/FibonacciPrimes.lean`. The problem is catalogued at https://en.wikipedia.org/wiki/Fibonacci_prime. LOCKED: solvers cannot modify this file.
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