Infinitely many odd k divide F_1 + ⋯ + F_k (Flynn-Connolly 2025)

For an odd prime p with p ≡ 2 (mod 3) and p ≡ ±2 (mod 5), and n = 2p or n = 4p, the Fibonacci number F_n is odd and F_{F_n + 2} ≡ 1 (mod F_n), so F_n divides F_1 + ⋯ + F_{F_n} = F_{F_n + 2} − 1; by Dirichlet's theorem there are infinitely many odd k with k ∣ F_1 + ⋯ + F_k, the conjecture of Fatehizadeh and Yaqubi (O. Flynn-Connolly, INTEGERS 25 (2025) A87). The statements are those of atlas-lean's FibonacciSumDivisibilityWanted. Proof: for even n the Pisano period of F_n divides 2n (Cassini); for such p, p ∣ F_{p+1} (from F_p ≡ (5/p), proved earlier in this library), so the period modulo 4p and 8p divides 2(p + 1).

Main results

• FibonacciSumDivisibility.period_fib_even: for even n, F_{k+2n} ≡ F_k (mod F_n)
• FibonacciSumDivisibility.fib_succ_prime_dvd: p ∣ F_{p+1} when p ≡ ±2 (mod 5)
• FibonacciSumDivisibility.flynn_connolly: Theorem 2 and Corollary 2 (atlas-lean wanted statements)

References

• O. Flynn-Connolly, «On the divisibility of sums of Fibonacci numbers», INTEGERS 25 (2025) A87; arXiv:2504.09938 v3, Thm 2 y Cor 2.
• A. Fatehizadeh, D. Yaqubi, «Average of the Fibonacci numbers», J. Integer Seq. 25 (2022), Art. 22.2.6 (la conjetura).
• facebookresearch/atlas-lean, WantedExt/NumberTheory/Recurrences/FibonacciSumDivisibilityWanted.lean (Apache-2.0).

def FibonacciSumDivisibility.Per (m T : ℕ) : Prop

F_{k+T} ≡ F_k (mod m) for all k.

Equations

• FibonacciSumDivisibility.Per m T = ∀ (k : ℕ), ↑(Nat.fib (k + T)) = ↑(Nat.fib k)

theorem FibonacciSumDivisibility.per_of_return {m : ℕ} (T : ℕ) (h0 : ↑(Nat.fib T) = 0) (h1 : ↑(Nat.fib (T + 1)) = 1) : Per m T

theorem FibonacciSumDivisibility.per_mul {m T : ℕ} (h : Per m T) (j : ℕ) : Per m (j * T)

theorem FibonacciSumDivisibility.per_crt {a b T : ℕ} (hc : a.Coprime b) (h1 : Per a T) (h2 : Per b T) : Per (a * b) T

theorem FibonacciSumDivisibility.period_fib_even (n : ℕ) (hn : Even n) (_hn1 : 1 < n) (k : ℕ) : Nat.fib (k + 2 * n) ≡ Nat.fib k [MOD Nat.fib n]

Proposition 2 (Flynn-Connolly): for even n > 1, F_{k+2n} ≡ F_k (mod F_n).

theorem FibonacciSumDivisibility.two_fib_succ (p : ℕ) [Fact (Nat.Prime p)] (hp2 : p ≠ 2) : 2 * ↑(Nat.fib (p + 1)) = 5 ^ (p / 2) + 1

The (0,0) entry of the Frobenius identity for the Fibonacci matrix (copy of the method of FibLegendre.fib_prime_eq_legendreSym, whose (0,1) entry gives F_p): 2 F_{p+1} = 5^{(p-1)/2} + 1.

theorem FibonacciSumDivisibility.not_square_two : ¬IsSquare 2

theorem FibonacciSumDivisibility.not_square_three : ¬IsSquare 3

theorem FibonacciSumDivisibility.legendreSym_five (p : ℕ) [Fact (Nat.Prime p)] (hp2 : p ≠ 2) (h5 : p % 5 = 2 ∨ p % 5 = 3) : legendreSym p 5 = -1

legendreSym p 5 = -1 for a prime p ≡ ±2 (mod 5).

theorem FibonacciSumDivisibility.fib_succ_prime_dvd (p : ℕ) (hp : Nat.Prime p) (h5 : p % 5 = 2 ∨ p % 5 = 3) : p ∣ Nat.fib (p + 1) ∧ ↑(Nat.fib p) = -1

Wall (case (5/p) = -1): for a prime p ≡ ±2 (mod 5), F_p ≡ -1 and p ∣ F_{p+1}.

theorem FibonacciSumDivisibility.per_p (p : ℕ) (hp : Nat.Prime p) (h5 : p % 5 = 2 ∨ p % 5 = 3) : Per p (2 * p + 2)

The period 2p + 2 = 2(p+1) modulo p.

theorem FibonacciSumDivisibility.per_four : Per 4 6

theorem FibonacciSumDivisibility.per_eight : Per 8 12

theorem FibonacciSumDivisibility.per_two : Per 2 3

theorem FibonacciSumDivisibility.per_4p {p : ℕ} (hp : Nat.Prime p) (hpodd : p % 2 = 1) (hp3 : p % 3 = 2) (hp5 : p % 5 = 2 ∨ p % 5 = 3) : Per (4 * p) (2 * p + 2)

theorem FibonacciSumDivisibility.per_8p {p : ℕ} (hp : Nat.Prime p) (hpodd : p % 2 = 1) (hp3 : p % 3 = 2) (hp5 : p % 5 = 2 ∨ p % 5 = 3) : Per (8 * p) (2 * p + 2)

theorem FibonacciSumDivisibility.fib_two_mul_mod {p : ℕ} (hp : Nat.Prime p) (hpodd : p % 2 = 1) (hp3 : p % 3 = 2) (hp5 : p % 5 = 2 ∨ p % 5 = 3) : 4 * p ∣ Nat.fib (2 * p) + 1

F_{2p} ≡ -1 (mod 4p).

theorem FibonacciSumDivisibility.fib_four_mul_mod {p : ℕ} (hp : Nat.Prime p) (hpodd : p % 2 = 1) (hp3 : p % 3 = 2) (hp5 : p % 5 = 2 ∨ p % 5 = 3) : 8 * p ∣ Nat.fib (4 * p) + 3

F_{4p} ≡ -3 (mod 8p).

theorem FibonacciSumDivisibility.fib_odd_of_not_dvd (n : ℕ) (h : n % 3 ≠ 0) : Nat.fib n % 2 = 1

F_n is odd when 3 ∤ n.

theorem FibonacciSumDivisibility.fibfib_mod (n : ℕ) (hn : Even n) (hn4 : 4 ≤ n) (h : 2 * n ∣ Nat.fib n + 1 ∨ 2 * n ∣ Nat.fib n + 3) : Nat.fib (Nat.fib n + 2) % Nat.fib n = 1

Core step: if F_n has period 2n and 2n ∣ F_n + 1 or 2n ∣ F_n + 3 (n ≥ 4 even) then F_{F_n+2} ≡ 1 (mod F_n).

theorem FibonacciSumDivisibility.theorem_two (p n : ℕ) (hp : Nat.Prime p) (hpodd : p % 2 = 1) (hp3 : p % 3 = 2) (hp5 : p % 5 = 2 ∨ p % 5 = 3) (hn : n = 2 * p ∨ n = 4 * p) : Nat.fib n % 2 = 1 ∧ Nat.fib (Nat.fib n + 2) % Nat.fib n = 1

Theorem 2 (Flynn-Connolly) for a prime p.

theorem FibonacciSumDivisibility.sum_fib_Icc (k : ℕ) : ∑ i ∈ Finset.Icc 1 k, Nat.fib i + 1 = Nat.fib (k + 2)

theorem FibonacciSumDivisibility.flynn_connolly : (∀ (p n : ℕ), Nat.Prime p → p % 2 = 1 → p % 3 = 2 → p % 5 = 2 ∨ p % 5 = 3 → n = 2 * p ∨ n = 4 * p → Nat.fib n % 2 = 1 ∧ Nat.fib (Nat.fib n + 2) % Nat.fib n = 1) ∧ {k : ℕ | Odd k ∧ k ∣ ∑ i ∈ Finset.Icc 1 k, Nat.fib i}.Infinite

Flynn-Connolly (2025). Theorem 2 and Corollary 2.