Erdős #601 — ordinal graphs: infinite path or full independent set

Statement

For which limit ordinals $\alpha$ is it true that if $G$ is a graph with vertex set $\alpha$ then $G$ must have either an infinite path or an independent set on a set of vertices with order type $\alpha$? (I.e. characterize all limit ordinals $\alpha$ satisfying the polarized-partition-style relation $\alpha \to (\alpha, \text{infinite path})^2$.)

Facts

- Prize \$500; status OPEN, "cannot be resolved with a finite computation" (erdosproblems.com/601, site-owner belief, verified by direct fetch 2026-07-02). - Falsifiable: no — this asks for a full characterization over all limit ordinals, and (as detailed below) the truth value genuinely varies with the model of set theory in the known range, so no single finite witness or single ZFC proof can "settle the general case" in the sense the prize asks for. - Origin: Erdős, Hajnal, Milner, "Set mappings and polarized partition relations" (1970) [EHM70]; Erdős, "On the combinatorial problems which I would most like to see solved" (1981) [Er81]; Erdős, "Some of my favourite problems which recently have been solved" (1982) [Er82e] — this is where the \$250/\$500 prize split is stated; Erdős, "Some problems on finite and infinite graphs" (1987) [Er87]. - Known results / best bounds (verified against erdosproblems.com/601 + cross-checked in the literature): - Erdős–Hajnal–Milner [EHM70] proved the positive relation holds for every limit ordinal $\alpha < \omega_1^{\omega+2}$ (ordinal exponentiation), via a set-mapping / free-set argument. - In [Er82e], Erdős offers \$250 for determining what happens exactly at $\alpha=\omega_1^{\omega+2}$ (the boundary case EHM70 leaves open) and \$500 for settling the general characterization for all limit ordinals. - Larson [La90] (*Martin's axiom and ordinal graphs: large independent sets or infinite paths*, Ann. Pure Appl. Logic 47(1):31-39, 1990) proved the positive relation holds for every limit ordinal $\alpha < 2^{\aleph_0}$ under Martin's axiom (MA); the forcing conditions used are finite independent sets (confirmed via Garti 2023, arXiv:2302.09492, §1, who recaps this explicitly). Since MA is consistent with $2^{\aleph_0}$ arbitrarily large, this in particular forces the positive relation at $\alpha=\omega_1^{\omega+2}$ under MA+$\lnot$CH. - Baumgartner–Larson [BL90] (*A diamond example of an ordinal graph with no infinite paths*, Ann. Pure Appl. Logic 47(1):1-10, 1990) constructed, from $\diamondsuit_{\aleph_1}$, an explicit counterexample graph — with no infinite path and no independent set of the required order type — for ordinals $\alpha$ in the range $\omega_1^{\omega+2} \le \alpha < \omega_2$ (per WebSearch-derived abstract summary and Garti 2023's recap of BL90's method; full text not independently obtained). This in particular gives a counterexample at $\alpha=\omega_1^{\omega+2}$ itself under $\diamondsuit_{\aleph_1}$. - Consequence for the \$250 sub-question: combining La90 and BL90, the truth of the relation at $\alpha=\omega_1^{\omega+2}$ is independent of ZFC — true under MA+$\lnot$CH, false under $\diamondsuit_{\aleph_1}$ (hence under CH/$V=L$). The erdosproblems.com page does not mark the \$250 as claimed/awarded, consistent with "determine what happens" not having a single ZFC answer. - Larson [Lar06] (*Partition relations on a plain product order type*, Ann. Pure Appl. Logic 144(1-3):117-125, 2006) revisits exactly this boundary and poses, as of 2006, the still-finer open question of whether CH alone (as opposed to the strictly stronger $\diamondsuit_{\aleph_1}$ used by BL90) decides the relation, both for $\alpha=\omega_1^{\omega+2}$ and for the closely related non-well-ordered type $\tau=\omega^*\cdot\omega_1$ (abstract via philpapers.org/rec/LARPRO-2). This is a live, more refined open sub-question directly in this problem's neighborhood. - Garti [Gar23] (*Tiltan and graphs with no infinite paths*, arXiv:2302.09492, math.LO, 2023 — full text read) shows the club principle ("tiltan", $\clubsuit_{\aleph_1}$, strictly weaker than $\diamondsuit_{\aleph_1}$) is *consistent with* the positive relation for the related order type $\tau=\omega^*\cdot\omega_1$, answering a 2006 question of Larson's for that type. The proof machinery — Shelah's generalized Martin's axiom at $\aleph_2$, Larson's "clean columns" technique, the Erdős–Dushnik–Miller theorem, Hajnal's free-set theorem, elementary-submodel arguments, then a Lévy collapse of $\aleph_1$ — is the current state of the art for this whole family of problems and is directly reusable for the genuine-ordinal case of #601. Garti also poses a further open question (whether *superclub* is consistent with the relation) showing the research line is still actively moving as of Aug 2023. - No paper was found that raises EHM70's ZFC-provable threshold $\omega_1^{\omega+2}$, nor one that resolves the general characterization beyond the independence results above. - Formalized: No. erdosproblems.com/601 states "Formalised statement? No"; confirmed no 601.lean exists in google-deepmind/formal-conjectures (404 on direct fetch, 2026-07-02). - Related problems: Erdős #592 — characterize the countable partition ordinals — same $\alpha\to(\alpha,k)^2$-style ordinal partition calculus, different specific relation (countable partition ordinals for $K_3$/$K_\alpha$).

Literature state

Not resolved, and more specifically this looks like a problem whose "general case" may be inherently model-dependent rather than settle-able by a single ZFC theorem — the one concrete boundary point Erdős singled out ($\alpha=\omega_1^{\omega+2}$, the \$250 sub-question) is already known (via La90 + BL90, both 1990) to be independent of ZFC: true under Martin's axiom, false under $\diamondsuit_{\aleph_1}$. That leaves two live threads, neither closed: (1) Larson's 2006 refinement of whether CH alone (not full $\diamondsuit$) already forces the negative direction at $\omega_1^{\omega+2}$ — open as of the 2006 paper, and I found no later paper resolving it; (2) the full characterization for $\alpha \ge \omega_2$, which is untouched in every source found — all positive-direction proofs (La90 for arbitrary $\alpha<2^{\aleph_0}$, Garti 2023 pushing MA-type arguments up to $\aleph_2$-sized structures before collapsing) are bounded by continuum-sized machinery, and no unconditional (ZFC) result or even a further independence result is known above $\omega_2$-scale ordinals. The most recent directly relevant paper is Garti's Aug 2023 arXiv:2302.09492, which explicitly works in the immediate technical neighborhood (Larson's "clean columns," generalized MA, diamond-vs-club dichotomy) but for the related non-well-ordered order type $\omega^*\cdot\omega_1$ introduced by Larson (2006), not literally the well-ordered-ordinal case of #601 — so it is evidence of an active research programme using the right tools, not a direct resolution. No AI/LLM/automated-theorem-prover contribution was found anywhere in this literature; the DeepMind formal-conjectures repository has no Lean statement for this problem at all (confirmed 404), unlike sibling problem Erdős #592 — characterize the countable partition ordinals which at least has an unproved statement scaffold.

Attack surface

- Mode: literature-resolution (chase Garti/Shelah/Larson citation trail forward from 2023 for any further movement, and specifically hunt for a paper resolving Larson's 2006 "does CH alone decide it" question) + derivation+formalization (any actual new theorem needs a real forcing/combinatorial construction, not a search). - Concrete first experiment: not a finite computation (falsifiability: not-finite). The realistic first moves are (1) obtain the full text of Larson [La90], [Lar06] and Baumgartner–Larson [BL90] (currently only abstracts/secondary summaries were accessible) to pin down exactly which forcing/diamond machinery is used and whether it can be pushed past $\omega_2$; (2) adapt Garti's 2023 "clean columns + generalized MA + Lévy collapse" architecture (arXiv:2302.09492 §2) from the order type $\omega^*\cdot\omega_1$ back to genuine well-ordered limit ordinals $\alpha$ in the EHM70 gap $[\omega_1^{\omega+2}, \omega_2)$ and beyond, to see whether the CH-alone question Larson posed in 2006 is tractable with this newer toolkit; (3) as a scoping step, formalize the problem statement in Lean (there is currently none) mirroring the pattern used for Erdős #592 — characterize the countable partition ordinals, to at least make partial/conditional results checkable. - Oracle: none mechanical — this is a set-theoretic independence-flavored question; the "oracle" for any claimed partial result is a human/formal forcing proof, in principle checkable in a proof assistant once a statement scaffold exists (none does yet for #601, unlike #592). - Feasibility: honest read: famous-and-hard, not in reach for a finite-search or SAT-style attack, and possibly not even resolvable as a single ZFC theorem. This is a 55+ year old set-theory problem (1970 EHM, 1990 Larson/Baumgartner-Larson, 2006 Larson, 2023 Garti) sitting exactly at the diamond-vs-Martin's-axiom fault line that governs a whole family of ordinal/uncountable-graph problems. The one concretely promising, non-speculative thread is Garti's 2023 tiltan machinery — worth a careful read-and-adapt rather than an independent attack, and worth citation-tracking forward for any 2024-2026 follow-up.

Related

- Erdős #592 — characterize the countable partition ordinals — sibling ordinal-partition-calculus problem ($\alpha\to(\alpha,3)^2$ for $\alpha=\omega^\beta$, countable partition ordinals); same general arrow-notation framework, different specific relation and largely disjoint technique (Schipperus/Chang/Specker topological-Ramsey-space constructions vs. this problem's diamond/Martin's-axiom forcing dichotomy) — useful as a contrast case for how "characterize all $\alpha$" ordinal problems get attacked. - Ordinal partition calculus — arrow notation $\\alpha\\to(\\alpha,m)^2$ and the self-partitioning-ordinal program — the general $\alpha\to(\alpha,\beta)^\gamma$ arrow-notation framework both this problem and Erdős #592 — characterize the countable partition ordinals live in. - concept/martins-axiom — Larson's [La90] positive-direction tool; forces the relation for all $\alpha<2^{\aleph_0}$. - concept/diamond-principle — Baumgartner–Larson's [BL90] negative-direction tool ($\diamondsuit_{\aleph_1}$); builds counterexamples in $[\omega_1^{\omega+2},\omega_2)$. - concept/club-principle — "tiltan" ($\clubsuit_{\aleph_1}$), strictly weaker than diamond; Garti (2023) shows it is *compatible* with the positive relation for the related type $\omega^*\cdot\omega_1$, the key recent structural result in this neighborhood. - concept/generalized-martins-axiom — Shelah's higher-cardinal MA generalization (forcing conditions: countable independent sets, chain condition via a club-guessing argument), the engine of Garti's $\aleph_2$-level positive theorem before collapsing to $\aleph_1$. - concept/erdos-dushnik-miller-theorem — $\lambda\to(\lambda,\omega)^2$ for every infinite cardinal $\lambda$; used as a black-box dichotomy lemma inside both Larson's and Garti's proofs. - concept/hajnals-free-set-theorem — set-mapping free-set extraction lemma; used by EHM70's original 1970 proof and again inside Garti's 2023 "clean columns" reduction. - concept/elementary-submodel-argument — countable elementary submodel technique used to prove the path-extraction lemma ($\omega_1\to_{\rm asp}(\omega)^2_{\omega\times\omega}$, Garti 2023 Lemma 1.4) underlying the forcing chain-condition proof. - Machine formalization of infinitary combinatorics proofs (Isabelle/HOL, Lean) — currently absent for this problem (no Lean/Isabelle statement exists, unlike Erdős #592 — characterize the countable partition ordinals); a natural first scaffolding step.