1. FormalConjectures
  2. ErdosProblems
  3. «219»
/- Copyright 2025 The Formal Conjectures Authors. Licensed under the Apache License, Version 2.0 (the "License"); you may not use this file except in compliance with the License. You may obtain a copy of the License at https://www.apache.org/licenses/LICENSE-2.0 Unless required by applicable law or agreed to in writing, software distributed under the License is distributed on an "AS IS" BASIS, WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. See the License for the specific language governing permissions and limitations under the License. -/ import FormalConjecturesUtil

Erdős Problem 219

Reference: erdosproblems.com/219

namespace Erdos219

The set of arithmetic progressions of primes

def primeArithmeticProgressions : Set (Set ℕ) := {s | (∀ p ∈ s, p.Prime) ∧ ∃ l > 0, s.IsAPOfLength l} @[category test, AMS 5 11] theorem primeArithmeticProgression_3_5_7 : {3, 5, 7} ∈ primeArithmeticProgressions := ⊢ {3, 5, 7} ∈ primeArithmeticProgressions ⊢ (Nat.Prime 3 ∧ Nat.Prime 5 ∧ Nat.Prime 7) ∧ ∃ x x_1, {3, 5, 7} = {x_2 | ∃ n < 3, x + n * x_1 = x_2} refine ⟨⊢ Nat.Prime 3 ∧ Nat.Prime 5 ∧ Nat.Prime 7 All goals completed! 🐙, ⟨3, 2, Set.ext fun x => ?_⟩⟩ refine ⟨?_, fun ⟨w, ⟨hl, hr⟩⟩ => x:ℕx✝:x ∈ {x | ∃ n < 3, 3 + n * 2 = x}w:ℕhl:w < 3hr:3 + w * 2 = x⊢ x ∈ {3, 5, 7} x:ℕx✝:x ∈ {x | ∃ n < 3, 3 + n * 2 = x}w:ℕhl:0 < 3hr:3 + 0 * 2 = x⊢ x ∈ {3, 5, 7}x:ℕx✝:x ∈ {x | ∃ n < 3, 3 + n * 2 = x}w:ℕhl:1 < 3hr:3 + 1 * 2 = x⊢ x ∈ {3, 5, 7}x:ℕx✝:x ∈ {x | ∃ n < 3, 3 + n * 2 = x}w:ℕhl:2 < 3hr:3 + 2 * 2 = x⊢ x ∈ {3, 5, 7} x:ℕx✝:x ∈ {x | ∃ n < 3, 3 + n * 2 = x}w:ℕhl:0 < 3hr:3 + 0 * 2 = x⊢ x ∈ {3, 5, 7}x:ℕx✝:x ∈ {x | ∃ n < 3, 3 + n * 2 = x}w:ℕhl:1 < 3hr:3 + 1 * 2 = x⊢ x ∈ {3, 5, 7}x:ℕx✝:x ∈ {x | ∃ n < 3, 3 + n * 2 = x}w:ℕhl:2 < 3hr:3 + 2 * 2 = x⊢ x ∈ {3, 5, 7} All goals completed! 🐙⟩ ⊢ 3 ∈ {x | ∃ n < 3, 3 + n * 2 = x}⊢ 5 ∈ {x | ∃ n < 3, 3 + n * 2 = x}⊢ 7 ∈ {x | ∃ n < 3, 3 + n * 2 = x} ⊢ 3 ∈ {x | ∃ n < 3, 3 + n * 2 = x} All goals completed! 🐙 ⊢ 5 ∈ {x | ∃ n < 3, 3 + n * 2 = x} simpa using ⟨1, ⊢ 1 < 3 ∧ 3 + 1 * 2 = 5 All goals completed! 🐙⟩ ⊢ 7 ∈ {x | ∃ n < 3, 3 + n * 2 = x} simpa using ⟨2, ⊢ 2 < 3 ∧ 3 + 2 * 2 = 7 All goals completed! 🐙⟩ @[category test, AMS 5 11] theorem not_primeArithmeticProgression_1_2 : ¬{1, 2} ∈ primeArithmeticProgressions := ⊢ {1, 2} ∉ primeArithmeticProgressions ⊢ Nat.Prime 1 → Nat.Prime 2 → ∀ (x : ℕ∞), 0 < x → ¬{1, 2}.IsAPOfLength x All goals completed! 🐙 @[category API, AMS 5 11] theorem empty_not_primeArithmeticProgression : ∅ ∉ primeArithmeticProgressions := ⊢ ∅ ∉ primeArithmeticProgressions All goals completed! 🐙 @[category API, AMS 5 11] lemma singleton_mem_primeArithmeticProgressions {p : ℕ} (hp : p.Prime) : {p} ∈ primeArithmeticProgressions := p:ℕhp:Nat.Prime p⊢ {p} ∈ primeArithmeticProgressions simpa [primeArithmeticProgressions, hp] using ⟨1, one_pos, p:ℕhp:Nat.Prime p⊢ {p}.IsAPOfLength 1 All goals completed! 🐙⟩ @[category API, AMS 5 11] lemma pair_mem_primeArithmeticProgressions {p q : ℕ} (hp : p.Prime) (hq : q.Prime) (hpq : p < q) : {p, q} ∈ primeArithmeticProgressions := p:ℕq:ℕhp:Nat.Prime phq:Nat.Prime qhpq:p < q⊢ {p, q} ∈ primeArithmeticProgressions p:ℕq:ℕhp:Nat.Prime phq:Nat.Prime qhpq:p < qn:ℕh:q = p + n + 1⊢ {p, q} ∈ primeArithmeticProgressions simpa [primeArithmeticProgressions, hp, hq] using ⟨2, p:ℕq:ℕhp:Nat.Prime phq:Nat.Prime qhpq:p < qn:ℕh:q = p + n + 1⊢ 0 < 2 All goals completed! 🐙, Nat.isAPOfLength_pair hpq⟩

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

@[category research solved, AMS 5 11] theorem declaration uses 'sorry'erdos_219 : answer(True) ↔ ∀ N : ℕ, ∃ l ∈ primeArithmeticProgressions, N ≤ ENat.card l := ⊢ True ↔ ∀ (N : ℕ), ∃ l ∈ primeArithmeticProgressions, ↑N ≤ ENat.card ↑l All goals completed! 🐙 end Erdos219