Research notes on every problem, and a library of the papers behind them. Built from the open erdos repository.
Updated
Problem 1187
claims/: The 3 claim pages of Problem 1187, one per claimant's result; the problem's standing derives from them.
Statement. Let . Is it true that, in any finite colouring of the integers, there are monochromatic arithmetic progressions of primes of length ?
Are there monochromatic arithmetic progressions of length whose common difference is a prime?
Formulation. The second question is read, as the site's commentary and the formal-conjectures statement read it, with the first question's quantifier: whether, for , every finite coloring of the integers has a monochromatic -term progression whose common difference is a prime. Read as asking about some coloring, it would be trivially yes (one color).
Status. Claimed. The site labels the problem SOLVED, but the derived standing is claimed: the first question's yes is an accepted claim, while the second question's no rests only on the site's own modulo-4 argument and Kitamura's unbuilt Lean proof of it for the natural numbers, both pending claim pages, since the argument has no publication and the curator who labels the problem wrote it. The label is the site's (SOLVED, page last edited 8 April 2026, as of 2026-10-07). The two questions have different answers: the first is yes for every by the Green–Tao theorem [GrTa08], since some color class of a finite coloring has positive relative upper density in the primes and so contains -term progressions; the second is no, by giving each integer the color of its residue class modulo , under which two integers of one color differ by a multiple of , or with two colors by putting the residues in one class and in the other, which has no monochromatic -term progression with prime difference.
Source. erdosproblems.com/1187 with its discussion thread (as of 2026-10-07: page last edited 8 April 2026; empty proof-claims tab). Cite as: T. F. Bloom, Erdős Problem #1187, https://www.erdosproblems.com/1187.
References.
- [Er80] Erdős, Paul, A survey of problems in combinatorial number theory. Ann. Discrete Math. 6 (1980), 89-115; p. 93. Library home: erdos_1980_survey_problems_combinatorial_number_theory.
- [GrTa08] Green, Ben and Tao, Terence, The primes contain arbitrarily long arithmetic progressions. Ann. of Math. (2) 167 (2008), no. 2, 481-547, doi:10.4007/annals.2008.167.481. Library home: green_2008_primes_contain_arbitrarily_long_arithmetic_progressions.
Formalization. The formal-conjectures statement file
FormalConjectures/ErdosProblems/1187.lean,
added on 20 September 2026 and linked at the commit of 6 October 2026,
states both questions for colorings of the integers, the first as
answer(True) and the second as answer(False), with sorry bodies under
the category research solved; its formal_proof attributes point to
src/latest/ErdosProblems/Erdos1187.lean in Boris Alexeev's lean-proofs
repository, added on 17 August 2026, which declares itself a Lean
formalization of a solution to the problem with Ben Green and Terence Tao as
its informal authors and Codex and GPT-5.6 Sol as its formal authors; its
theorem erdos_1187 proves both answers, the first from the repository's
own Green–Tao theorem together with van der Waerden's theorem obtained
through Hales–Jewett, the second by the modulo- coloring. That file is
linked from
the Green–Tao claim page
as a self-declared formalization of their result. The discussion thread
also carries a Lean 4 development posted on 12 May 2026 by Kenta Kitamura,
who names Codex and GPT-5.5 xhigh as its assistants, which formalizes the
site's standard modulo- counterexample for colorings of the natural
numbers, the extension to colorings of the integers not formalized, together
with a Lean statement of the first question without a proof; its repository
is linked at a pinned commit from
its claim page.
This corpus has built and audited none of these, so none gives formalized
evidence.
Current assessment
The first question is yes and the second no. The standing is derived from the claim pages, one part per question. Green and Tao's theorem answers the first question yes for every , an accepted partial claim on its claim page, accepted on the refereed Annals publication. The modulo- coloring answers the second question no; it is the site's own argument, which the curator gives in the commentary and credits to nobody, and it has no publication, so it is pending on its claim page. Kitamura's Lean proof of it for the natural numbers, posted on the discussion thread on 12 May 2026, is pending on its claim page; this corpus has not built it. The problem is therefore claimed, answered: an accepted claim and pending claims together settle its two parts. No forum proof claim, release item or lead names the problem.
Linked library material
These entries are derived from explicit links on library pages. They are navigation only and do not by themselves record mathematical progress.