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
∀ {p : ℕ}, Nat.Prime p → {p} ∈ Erdos219.primeArithmeticProgressionsAPIStatement only, no proof