---

Claim. On 2026-06-23 Kenta Kitamura (forum name KentaKitamura) posted in the thread of Problem 176 a second Lean 4 development, for the displayed question $N(k,\sqrt k)\le C^k$. Its theorem erdos176SqrtNumber_le_report_bound, with the README's compact form Erdos176Lean.N176Sqrt_le_report_bound_explicit, states that for every $k\ge2$

$$N(k,\sqrt k)\le\left\lfloor\tfrac43(k^2-k+1)(k-1)\bigl(k(k-1)+1\bigr)\right\rfloor+1,$$

where the condition $\lvert\sum f\rvert\ge\sqrt k$ on a $k$-term progression is encoded as $k\le(\sum f)^2$, so that the bound is $O(k^5)$ and in particular $N(k,\sqrt k)\le C^k$. The development reuses the infrastructure of the author's $N(k,2)$ formalization, and its README reports that #print axioms lists only propext, Classical.choice and Quot.sound. The post discloses that the formalization and comment were prepared with assistance from Codex 5.5 using xhigh reasoning and ChatGPT 5.5 Pro.

Covers. The displayed question $N(k,\sqrt k)\le C^k$, answered yes with a polynomial bound. The result settles nothing for the question $N(k,ck)\le C^k$ with $0<c<1$ or for the request for good upper bounds in general; the question $N(k,2)\le C^k$ has its own claim page.

Depends on. Nothing in this wiki.

Standing. Claimed. Zach Hunter wrote in the thread on 1 April 2026 that Hunter and others had found an argument showing $N(k,c\sqrt k)=O(k^3)$ for some $c>0$; no note of that argument is known here, and a reply of 21 June 2026 to the author's first development remarks that the reconstructed argument generalizes to Hunter's bound. No comment on this development is recorded in the thread. The site labels the problem OPEN and its commentary does not record the bound, so no reviewed evidence is listed; nothing was built or audited here, so no formalized evidence is listed.