Erdős Problem 219

Reference: erdosproblems.com/219

def primeArithmeticProgressions : Set (List ℕ)

The set of arithmetic progressions of primes

Equations

• primeArithmeticProgressions = {l : List ℕ | l ≠ [] ∧ (∀ p ∈ l, Nat.Prime p) ∧ ∃ (step : ℕ), step ≠ 0 ∧ List.Chain' (fun (a b : ℕ) => b = step + a) l}

theorem singleton_mem_primeArithmeticProgressions {p : ℕ} (hp : Nat.Prime p) : [p] ∈ primeArithmeticProgressions

theorem pair_mem_primeArithmeticProgressions {p q : ℕ} (hp : Nat.Prime p) (hq : Nat.Prime q) (hpq : p < q) : [p, q] ∈ primeArithmeticProgressions

theorem erdos_219 : (∀ (N : ℕ), ∃ l ∈ primeArithmeticProgressions, N ≤ l.length) ↔ True

Are there arbitrarily long arithmetic progressions of primes? Solution: yes. Ref: Green, Ben and Tao, Terence, The primes contain arbitrarily long arithmetic progressions