Wiki
Wiki

Research notes on every problem, and a library of the papers behind them. Built from the open erdos repository.

Updated

Problem 984

../

claims/: The 1 claim page of Problem 984, one per claimant's result; the problem's standing derives from them.


Statement. Can N\mathbb{N} be 22-coloured such that if

{a,a+d,…,a+(k−1)d}\{a,a+d,\ldots,a+(k-1)d\}

is a kk-term monochromatic arithmetic progression then $k\ll_\epsilon a^\epsilon$ for all ϵ>0\epsilon>0?

Status. Proved. The label is the site's (PROVED, page last edited 4 April 2026, read 2026-10-07), with the commentary crediting Zach Hunter's proof on the discussion thread. The standing is derived from the claim page: the accepted claim is Hunter's 22-coloring of 10 August 2025, on its claim page, which gives every monochromatic kk-term progression starting at aa at most exp⁡((log⁡a)1/2+o(1))\exp((\log a)^{1/2+o(1)}) terms and is accepted on the site's label; no write-up outside the thread was found on 2026-10-07. Spencer's three-color version with a very slowly growing bound and Erdős's two-coloring with k≪a1−ck\ll a^{1-c} are the earlier results the site records.

Source. erdosproblems.com/984, accessed 2026-09-04; page and thread read 2026-10-07 (page last edited 4 April 2026; empty proof-claims tab). Cite as: T. F. Bloom, Erdős Problem #984, https://www.erdosproblems.com/984.

References.

Formalization. No formal-conjectures statement: the site's indicator reads No. A Lean 4 development in Boris Alexeev's lean-proofs repository declares itself a formalization of Hunter's proof and is linked on the claim page; it is not among the Lean the corpus has built and audited.

Current assessment

Settled by Hunter's two-coloring of 10 August 2025, accepted on the curator's credit. The site formulation above (page last edited 4 April 2026, read 2026-10-07) asks for a 22-coloring of N\mathbb{N} under which every monochromatic kk-term progression starting at aa has k≪ϵaϵk\ll_\epsilon a^\epsilon for every ϵ>0\epsilon>0. The answer is yes: Zach Hunter's coloring, posted on the discussion thread, gives every such progression at most exp⁡((log⁡a)1/2+o(1))\exp((\log a)^{1/2+o(1)}) terms by coloring the intervals [100t,100t+1)[100^t,100^{t+1}) with the off-diagonal van der Waerden colorings of Green and of Hunter, with the roles of the colors exchanged between odd and even tt. It is recorded on [[problems/additive_combinatorics/E0984/claims/2025_08_10_hunter|the claim page]] as an accepted full claim with reviewed as its only evidence: the site's curator credits the proof, and no write-up outside the thread was found on 2026-10-07. Earlier, Spencer had proved the three-color version with a very slowly growing bound in place of aϵa^\epsilon, and Erdős ([Er80], p. 92) reports a 22-coloring with k≪a1−ck\ll a^{1-c} for an absolute c>0c>0 and no nontrivial lower bound. Hunter's post names the exponent 1/21/2 as a barrier for the present constructions. A Lean 4 file in Boris Alexeev's lean-proofs repository, added 2026-08-18, declares itself a formalization of Hunter's solution and proves the statement with k≤A aϵk\le A\,a^\epsilon; it is linked on the claim page and is not among the Lean the corpus has built and audited, so it gives no formalized evidence. No forum 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.