---

Claim. The second question of Problem 1187 is answered no: there is a coloring with finitely many colors in which no monochromatic $k$-term arithmetic progression, $k\ge3$, has a prime common difference. The claimed result is the Lean 4 development that Kenta Kitamura (forum username KentaKitamura, repository KitaKen1) posted on the problem's discussion thread on 12 May 2026, prepared, as the post and the repository state, with Codex and GPT-5.5 xhigh. The development states both questions of the problem in Lean for colorings of the natural numbers, with progressions $a+id$ for natural $a$ and $d$, and proves the second one false by the coloring that assigns each natural number its residue modulo $4$: two numbers of one color differ by a multiple of $4$, which is never prime, so no color class holds even a pair with prime difference. The first question is stated without a proof. The repository's README presents the development as a formalization of the standard modulo-$4$ counterexample described on the problem page, which is the site's own answer on its claim page; it is not a formalization of Green and Tao's theorem on the accepted page.

Submission note. Posted to the site's forum by Kenta Kitamura on 12 May 2026:

I have formalized in Lean the standard mod 4 counterexample for the second part of [1187]. AI assistance disclosure: this formalization was prepared with assistance from Codex, GPT-5.5 xhigh.

Lean file / repository: GitHub repository Typecheck information: Lean 4 Web version

Covers. The second question only, in its natural-number form: a finite coloring of the natural numbers need not contain a monochromatic $k$-term progression with prime common difference. The same residue coloring, defined on all integers, is the integer-form counterexample, since two integers in one residue class modulo $4$ differ by a multiple of $4$, which is never prime; the development states and proves only the natural-number form, and that extension is not formalized. It says nothing about the first question, monochromatic progressions of primes, which Green and Tao's theorem answers yes.

Depends on. Nothing in this wiki.

Standing. Claimed: the development is linked at a pinned commit, since the post gives no commit, and this corpus has not built or audited it, so it gives no formalized evidence; no reviewer independent of the author has recorded accepting it, since the curator's commentary gives the same coloring on its own account and does not credit this proof. The problem's standing is claimed through the pending second-question claims together with the accepted first-question claim.