Erdős Problem 219

Reference: erdosproblems.com/219

def Erdos219.primeArithmeticProgressions : Set (Set ℕ)

The set of arithmetic progressions of primes

Equations

• Erdos219.primeArithmeticProgressions = {s : Set ℕ | (∀ p ∈ s, Nat.Prime p) ∧ ∃ l > 0, s.IsAPOfLength l}

theorem Erdos219.primeArithmeticProgression_3_5_7 : {3, 5, 7} ∈ primeArithmeticProgressions

theorem Erdos219.not_primeArithmeticProgression_1_2 : {1, 2} ∉ primeArithmeticProgressions

theorem Erdos219.empty_not_primeArithmeticProgression : ∅ ∉ primeArithmeticProgressions

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

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

theorem Erdos219.erdos_219 : (∀ (N : ℕ), ∃ l ∈ primeArithmeticProgressions, ↑N ≤ ENat.card ↑l) ↔ True

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