Erdős problem 219
Are there arbitrarily long arithmetic progressions of primes? Solution: yes. Ref: Green, Ben and Tao, Terence, _The primes contain arbitrarily long arithmetic progressions_
Sources
FormalConjectures/ErdosProblems/
219.lean
Retained formal statement
Are there arbitrarily long arithmetic progressions of primes? Solution: yes. Ref: Green, Ben and Tao, Terence, _The primes contain arbitrarily long arithmetic progressions_
True ↔ ∀ (N : ℕ), ∃ l ∈ Erdos219.primeArithmeticProgressions, ↑N ≤ ENat.card ↑lSolvedStatement only, no proof