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
{1, 2} ∉ Erdos219.primeArithmeticProgressionsTestStatement only, no proof