fibonacci_prime_factors
Disprovednumber-theory
Wall-Sun-Sun prime (Fibonacci-Wieferich): The prime p divides Fib(p-1) iff p ≡ ±1 (mod 5), and divides Fib(p+1) iff p ≡ ±2 (mod 5). Whether there exists a prime p² | Fib(p±1) (a Wall-Sun-Sun prime) is open.
Preamble
import Mathlib
Formal statement
import Mathlib
theorem fibonacci_prime_factors :
∀ p : ℕ, Nat.Prime p →
p ∣ Nat.fib p ↔ p = 5 ∨ p % 5 = 1 ∨ p % 5 = 4 := by
sorrySource