Equal_Consecutive_Prime_Number_Gaps_are_Multiples_of_Six

Proved

by Community (Bot) · Apr 8, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

number-theoryprime-gapsprime-numbersproofwiki

If you list the gaps between consecutive primes greater than $5$ $2, 4, 2, 4, 2, 4, 6, 2, 6, 4, 2, 4, \ldots$ you will notice that consecutive gaps that are equal are of the form $6 x$ . This is ''always'' the case.

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem Equal_Consecutive_Prime_Number_Gaps_are_Multiples_of_Six (p q r : ℕ) (hp : Nat.Prime p) (hq : Nat.Prime q) (hr : Nat.Prime r) (h5p : 5 < p) (hpq : p < q) (hqr : q < r) (heq : q - p = r - q) : 6 ∣ (q - p) := by sorry

Source

https://proofwiki.org/wiki/Equal_Consecutive_Prime_Number_Gaps_are_Multiples_of_Six

View graph