---

Claim. The answer to Problem 219 is yes: for every $k\ge1$ the primes contain an arithmetic progression of $k$ terms. The claimed result is Theorem 1.1 of Ben Green and Terence Tao, The primes contain arbitrarily long arithmetic progressions, which states more: for every $k$ there are infinitely many $k$-term arithmetic progressions of primes. Theorem 1.2 of the same paper strengthens this to every subset of the primes of positive relative upper density. The proof combines Szemerédi's theorem with a transference principle, which carries Szemerédi's theorem from dense subsets of the integers to sets of positive relative density with respect to a pseudorandom measure, and the Goldston–Yıldırım sieve estimates, which place the primes inside such a measure concentrated on almost primes; it gives at least $(\gamma(k)+o(1))N^2/\log^kN$ progressions of $k$ primes up to $N$. The source card green_2008_primes_contain_arbitrarily_long_arithmetic_progressions digests the paper.

Acceptance. Refereed publication: Ann. of Math. (2) 167 (2008), no. 2, 481--547, doi:10.4007/annals.2008.167.481. Reviewed: the site's curator, Thomas Bloom, labels the problem proved and credits [GrTa08] in the problem page's commentary (page last edited 4 April 2026; site export of 2026-10-06); he is independent of the authors. For context, not as acceptance evidence: Guy's 2004 collection, in its stop-press note on the announcement, records his own view that the proof was almost certainly complete, and the theorem has been the accepted answer since its publication. The card's text is the arXiv version (v1 posted 8 April 2004, the date of this page; v6 of 23 September 2007).

Formalization. The two formalization links are a Lean 4 development in Boris Alexeev's repository lean-proofs (Lean v4.33.0, Mathlib v4.33.0, pinned at the commit of 2026-09-07) that declares itself a formalization of this theorem: the module src/latest/ErdosProblems/Erdos219.lean (first added 2026-08-16) proves Erdos219.erdos_219, that for every N : ℕ there is a set of primes that is an arithmetic progression of positive length with at least N elements, by taking a progression of max 1 N primes from GreenTao.green_tao and packaging it as a set. Its header names Green and Tao as the informal authors, the formal-conjectures authors for the statement, and Codex and GPT-5.6 Sol as the formal proof authors. The theorem green_tao, in src/latest/Wikipedia/GreenTao.lean of the same repository (added the same day), states that the set of primes contains arithmetic progressions of every finite length and is proved from the repository's Wikipedia.SzemeredisTheorem development through a transference statement for the primes with a linear-forms majorant and a pattern-removal input; the file closes with #print axioms green_tao and records no output. The site's Lean qualifier, which the community database lists as of its last update (2026-08-23), refers to this development, added on 2026-08-16; the formal-conjectures statement erdos_219 has named the Erdos219 module as its formal proof since 2026-09-13. This corpus has not built or audited the development, so the page lists no formalized evidence and the acceptance rests on the refereed paper and the curator's credit. The OpenAI release's reciprocal-sum route to the same answer has its own claim page.