Erdős·erdos:190
Erdős 190
No independent check recorded yet. A formal artifact, declaration or published object is attached, but no rebuild of it is recorded here.
A Palomar registration names this problem. It is shown below but not counted as a check of the claim.
Fidelity F2: The correspondence is declared through a Comparator challenge, an alignment table and written divergences.
additive combinatorics, arithmetic progressions·Source
AI activity
How grades workNo AI contribution recorded against this statement.
Claimed on erdosproblems.com
1Proof claims posted on erdosproblems.com, which says that listing a claim “is no guarantee of proof correctness”. The register records who claims what, with which systems, and links to each claim there. Nobody has examined them, and none counts in the register's totals.
Fidelity
How fidelity is gradedF2 declared. The correspondence is declared through a Comparator challenge, an alignment table and written divergences.
Checks
1-
verified·Palomar
Registered by Palomar at be43a3ea: Comparator confirmed 4 theorems prove the recorded statement within Palomar's axiom policy, replayed through Lean's kernel and the independent nanoda kernel. The project names this problem, which does not establish that it proves the result claimed here, so it is not counted as a check of it
Declared by the projects
1As each project's formalization.yaml states it.
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
- authors
- Ji Ho Bae
- method
- agent
- review
- agent-reviewed (Ji Ho Bae (self-assessment), Palomar registry automated editorial review (codex:gpt-5.6-sol))
- axioms
- Classical.choice, Quot.sound, propext
- sorry
- 0 unproved goals declared
- results
- 4 main results named, checked with Comparator, with an alignment table
- sources
- A resolution of Erdős Problem #190: the canonical van der Waerden number satisfies H(k)^{1/k}/k → ∞ — formalizes, authors participated; Erdős Problem #190 (erdosproblems.com) — background; Old and new problems and results in combinatorial number theory: van der Waerden's theorem and related topics — background; Three-color van der Waerden numbers grow super-exponentially — background
- related
- yidiq7/ProbMethodCombinatorics — builds-on
- divergences
- The formal statements are the qualitative statement of the paper (Corollary 1.2), phrased for every canonical N so as not to assume the existence of H(k); divergence alone does not entail a statement about H(k), and the conclusion H(k) > (Ck)^k for all large k is formalized only under the explicit existence hypothesis (H_divergence). The paper's Proposition 4.1 uses r₀ = ⌊k/log k⌋ and gives the rate √k/log k; the formalization uses r₀ = ⌊k/3⌋, which avoids real analysis in the asymptotic step and gives the rate k^{1/6−o(1)}. The Erdős–Lovász base is formalized with the cruder constant r^(k−1)/(16k²) (the paper has r^(k−1)/(16k)), obtained with the dependency-degree bound k²N in the local lemma; only the shape r^(k−1)/poly(k) matters. [N] is modelled as Fin N (0-indexed), which does not affect any statement. The paper's main theorem (the explicit constant 1/e and ε(k), via the Baker–Harman–Pintz prime-gap theorem) is not formalized.
- checked by
- Palomar
Follow and discuss
All discussionFollow this problem
An email when it has a new claim, check, bounty or discussion. You confirm once and can stop with one click.
Discussion and bounties for this problem load here.
Seen recently
What the monitors picked up in the last thirty days, not yet graded.
Something wrong or missing here? Request a correction or add a claim, with its sources.
Claims and corrections from readers
All of themFormal material
Formal statements · 0
No formal statement located.
Cited proofs · 0
No proof artifact cited by the formal record.
Also known as · 1
- https://www.erdosproblems.com/190
Cite this record
qed.bot, “Erdős 190”, https://qed.bot/s/erdos-190, as of 30 Sep 2026.