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.
Does the formal statement say what was claimed?
F2 declared The correspondence is declared through a Comparator challenge, an alignment table and written divergences.
Computed from what the project declares and what the register holds, never from reading the mathematics. How fidelity is graded.
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
1Read from each project's formalization.yaml. A declaration is what the authors say about their own work, recorded so that a check can confirm or contradict 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 discussionGet an email when this problem moves
A new claim, a check, a bounty or a discussion. One link to confirm, one click to stop.
Discussion and bounties for this problem load here.
Formal 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