Erdős Problem #176 — Let $N(k,\ell)$ be the minimal $N$ such that for any $f:\{1,\ldots,N\}\to\{-1,1\}$ there must exist a $k$-term arithmetic progression $P$ such that…

Erdős Problem $176$ asks for upper bounds on the least $N(k,ll)$ forcing a $k$-term arithmetic progression whose signed sum has absolute value at least $ll$. In particular, it asks whether $N(k,2)\leq C^k$; the problem page continues to label this open.

Known results

• Spencer, 1973: if $k=2^t m$ with $m$ odd, then $N(k,1)=2^t(k-1)+1$.
• Erdős, 1963: for every $c>0$, $N(k,ck)>(1+\alpha_c)^k$, with $\alpha_c\to0$ as $c\to0$ and $\alpha_c\to\sqrt{2}-1$ as $c\to1$.
• A local-lemma argument gives $N(k,ck)\gg 2^k/[k^{O(1)}\sum_{i>(1+c)k/2}\binom{k}{i}]$, hence $(2-o(1))^k$ lower bounds as $c\to1$.

Recent claimed formalizations

A comment claims Lean formalizations proving $N(k,2)=O(k^3)$ and $N(k,\sqrt{k})=O(k^5)$, with explicit bounds and separate small cases. If correct, the first would settle the stated exponential question; however, these remain unverified comment-level claims, with no independent published confirmation. Small computations instead suggest the conjecture $N(k,2)\leq k^2$.

Current status (as of July 2026): The exponential lower bounds and classical special cases are known, while the claimed polynomial upper bounds for $N(k,2)$ and $N(k,\sqrt{k})$ remain unverified; the problem is officially open.