---

Claim. On 2026-06-21 Kenta Kitamura (forum name KentaKitamura) posted in the thread of Problem 176 a Lean 4 development for the displayed question $N(k,2)\le C^k$. Its theorem Erdos176Lean.erdos176Number_le_report_bound states that for every $k\ge5$

$$N(k,2)\le\left\lfloor\frac{2(k^2-1)(k-1)(2k+1)}{k-3}\right\rfloor+1,$$

where $N(k,2)$ is the least $N$ such that every $f:\{0,\dots,N-1\}\to\{-1,1\}$ has a $k$-term arithmetic progression with positive common difference inside $[0,N)$ on which $\lvert\sum f\rvert\ge2$. Its README reports that #print axioms lists only propext, Classical.choice and Quot.sound, and its appendix records the finite checks $N(2,2)=3$, $N(3,2)=9$ and $N(4,2)=13$, each with its own Lean file. So $N(k,2)=O(k^3)\le C^k$ for every $k\ge2$; no $N(1,2)$ exists, since a one-term sum has absolute value $1$. The post discloses that the computation and comment were prepared with assistance from Codex 5.5 using xhigh reasoning and ChatGPT 5.5 Pro.

Covers. The displayed question $N(k,2)\le C^k$, answered yes with a polynomial bound. For even $k$ this already follows from Spencer's formula $N(k,1)=2^t(k-1)+1$ for $k=2^tm$ with $m$ odd, through the parity identity $N(k,2)=N(k,1)$ that a comment in the thread noted on 19 March 2026, so the new case is odd $k$. The result settles nothing for the question $N(k,ck)\le C^k$ with $0<c<1$ or for $N(k,\sqrt k)$, which has its own claim page.

Depends on. Nothing in this wiki.

Standing. Claimed. A reply in the thread the same day reports a screening check that found the proof correct and remarks that the argument, as reconstructed, generalizes to the $O(k^3)$ bound for $N(k,c\sqrt k)$ that Zach Hunter had announced in the thread on 1 April 2026 without a note, so that Kitamura may have found Hunter's argument independently. That check is commentary on a problem the site labels OPEN and not an acceptance, so no reviewed evidence is listed. Nothing was built or audited here, so no formalized evidence is listed. The site's commentary does not record the bound.