{"id":"palomar/PALOMAR-2026-09-15-000003","url":"https://github.com/jbaelaw/erdos190-lean/tree/be43a3ead08a9d9af352cf296d284dd3468ca805","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-09-15-000003-v1.json","repo":"https://github.com/jbaelaw/erdos190-lean","tags":["math.CO","math.NT","msc:05D10","msc:11B25","msc:05C65","combinatorics","ramsey-theory","van-der-waerden","lean-formalization"],"score":0,"title":"Erdős Problem 190: every canonical N exceeds (Ck)^k for large k, and H(k)^{1/k}/k → ∞ under the existence hypothesis — a Lean 4 formalization of the qualitative statement of arXiv:2604.20588","trust":"high","domain":"math.CO","source":"palomar","authors":["Ji Ho Bae"],"reviews":0,"subject":"math.CO","summary":"A Lean 4 formalization, against Mathlib, of the qualitative statement of J. H. Bae, \"A resolution of Erdős Problem #190: the canonical van der Waerden number satisfies H(k)^{1/k}/k → ∞\" (arXiv:2604.20588, v2), Corollary 1.2, via the elementary argument of its Section 4.3. Let H(k) be the least N such that every finite colouring of {1,…,N} contains a monochromatic or a rainbow k-term arithmetic progression; Erdős and Graham (1979) asked whether H(k)^{1/k}/k → ∞ (Problem 190 in Bloom's database). The compared theorems state that for every C there is K such that for all k ≥ K every N for which…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-09-15","reactions":{},"formalized":true,"formalizes":[{"title":"A resolution of Erdős Problem #190: the canonical van der Waerden number satisfies H(k)^{1/k}/k → ∞","identifier":"https://arxiv.org/abs/2604.20588","relationship":"formalizes"},{"title":"A new lower bound for van der Waerden numbers","identifier":"https://doi.org/10.1016/j.ejc.2017.10.007","relationship":"adapts"},{"title":"Problems and results on 3-chromatic hypergraphs and some related questions","identifier":"Colloq. Math. Soc. János Bolyai 10 (1975), 609–627","relationship":"adapts"}]}