---

Claim. Ji Ho Bae, in a preprint posted to Zenodo and arXiv on 2026-04-22 ([[../library/additive_combinatorics/bae_2026_resolution_erdos_problem_190_via_erdos/_index|source card]]), proves that there is an absolute $k_0$ such that for every $k\ge k_0$

$$\frac{H(k)^{1/k}}{k}\ \ge\ \Bigl(\frac1e-\varepsilon(k)\Bigr)\frac{k}{\log k}, \qquad \varepsilon(k)=O\bigl(k^{-0.475}\log k\bigr),$$

its Theorem 1.1, so that $H(k)\ge k^{(2-o(1))k}$ and, by its Corollary 1.2, $H(k)^{1/k}/k\to\infty$. This answers the displayed question of Problem 190, as its precise Statement reads it, with a rainbow $k$-term progression, in the affirmative. The proof is short and uses only known ingredients: the pigeonhole reduction $H(k)\ge W(k-1,k)$ (a coloring with $k-1$ colors has no rainbow $k$-term progression), the Erdős–Lovász local-lemma bound $W(r,k)\gg r^{k-1}/k$ applied with a color count $r_0=\lfloor k/\log k\rfloor$ that grows with $k$, the restricted Blankenship–Cummings–Taranchuk recurrence iterated up to a prime $p^*\le k-1$, and the Baker–Harman–Pintz prime-gap theorem as the only analytic input. The paper notes that no upper bound on $H(k)^{1/k}/k$ beyond the existence of $H(k)$ is known, so the open-ended request to estimate $H(k)$ is not closed by the result.

Submission note. The Palomar registry's description of entry PALOMAR-2026-09-15-000003:

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 [N] is canonical for k satisfies (Ck)^k < N (divergence, and its Filter.Eventually form); this is a statement about canonical N only and by itself says nothing about H(k) (it holds vacuously for a k with no canonical N, where H(k) = sInf ∅ = 0). Combined with the existence of a canonical N for every k — the Erdős–Graham theorem, via Szemerédi's theorem, which is not formalized — it gives H(k) > (Ck)^k for all large k, i.e. H(k)^{1/k}/k → ∞; that conditional conclusion is stated as H_divergence, with the existence as an explicit hypothesis on H(k) = sInf {N | canonical}. The fourth compared theorem is the explicit bound behind the argument: for k ≥ 12 there is a prime p with (k−1)/2 < p ≤ k−1 such that every canonical N exceeds p^(p − ⌊k/3⌋)·⌊⌊k/3⌋^(k−1)/(16k²)⌋ (integer divisions, as in the Lean statement). The proof composes the Erdős–Lovász lower bound W(r,k) − 1 ≥ r^(k−1)/(16k²) for van der Waerden numbers (obtained from the symmetric Lovász local lemma, applied with a number of colours r₀ = ⌊k/3⌋ growing with k), the restricted Blankenship–Cummings–Taranchuk recurrence W(r,k) − 1 ≥ p·(W(r−1,k) − 1) for primes r ≤ p ≤ k, Bertrand's postulate, and elementary asymptotics. The paper's main theorem, the explicit rate H(k)^{1/k}/k ≥ (1/e − ε(k))·k/log k obtained with the Baker–Harman–Pintz prime-gap theorem, is not formalized (that theorem is not available in Mathlib); the formalized argument gives the weaker rate k^{1/6−o(1)}, which suffices for the qualitative statement. The compared theorems depend only on propext, Classical.choice and Quot.sound.

Depends on. No page of this wiki: the proof's inputs are the published results named above, cited in the preprint.

Acceptance. Reviewed: the site's curator (T. F. Bloom) labels Problem 190 solved and, in the commentary last edited 2026-06-02, credits Bae with the bound $H(k)\ge k^{(2-o(1))k}$. Fox and Hunter, whose independent and stronger bound has its [[problems/additive_combinatorics/E0190/claims/2026_06_01_fox_hunter|own claim page]], write in their preprint that Bae's bound "also resolves the problem from [13]" (Fox and Hunter 2026, Section 1.1, where [13] is Erdős and Graham 1979). Two independent proofs by different methods therefore corroborate each other. Neither proof has a refereed publication so the evidence is reviewed only. A discussion-thread post of 2026-04-23 reports a routine check of the Zenodo manuscript that found no issues; it is not an independent review and adds nothing to the standing.

Formalization. Bae's Lean 4 repository, pinned above at its commit of 2026-09-15, states the qualitative form: for every $C$ there is $K$ such that for all $k\ge K$ every $N$ with the canonical property for $k$ exceeds $(Ck)^k$. By the author's own note on the site's proof-claims page (2026-09-15), the existence of such $N$ is a hypothesis of the formal statement, not a formalized theorem, and the Lean sources were to accompany a second arXiv version. The pinned commit records the repository's registration at the Palomar registry of Lean-verified results, entry PALOMAR-2026-09-15-000003, linked above. The community database (teorth/erdosproblems) lists the problem's formal status as Lean, as of its last update of 2026-09-15, through this repository, with the same note that the existence of $H(k)$ is not formalized. This project has not built the repository or audited its statement against the problem, so the formalization is recorded as a link and is not acceptance evidence.