Erdős #590 — ω^ω → (ω^ω, 3)² (Chang's ordinal partition theorem)

Statement

Let $\alpha = \omega^\omega$ (the infinite ordinal, i.e. the order type of $\{\omega^n : n<\omega\}$-indexed towers, equivalently the countable limit of $\omega, \omega^2, \omega^3,\dots$). Is it true that in any red/blue colouring of the edges of the complete graph $K_\alpha$ (i.e. of the pairs $[\alpha]^2$) there is either a red $K_\alpha$ (a subset of order type $\omega^\omega$, all of whose pairs are red) or a blue $K_3$ (a 3-element blue-monochromatic triangle)? In arrow notation: $\omega^\omega \to (\omega^\omega, 3)^2$.

A problem of Erdős and Rado. Erdős offered \$250 for the resolution [erdosproblems.com/590, LaTeX source].

Facts

- Prize: \$250. Status: PROVED (true). Formalized: yes, in Isabelle/HOL (google-deepmind/formal-conjectures Lean statement also exists per erdosproblems.com; the *proof* — not just the statement — was mechanically verified by Paulson et al.). - Necessary background fact: if an ordinal $\beta$ is not a power of $\omega$ (and not $0$), then $\beta = \gamma+\delta$ for some $\gamma,\delta<\beta$, from which $\beta \not\to (\beta,3)$ follows easily (arxiv.org/pdf/2104.11613, §2). So only the indecomposable ordinals — the powers of $\omega$ — are even candidate "partition ordinals," and #590/#591/#592 are exactly the question of which powers of $\omega$ work. - Precursors (Specker, "Teilmengen von Mengen mit Relationen," Comment. Math. Helv. 1957 [Sp57]): $\omega^2 \to (\omega^2,3)^2$ holds, but $\omega^n \not\to (\omega^n,3)^2$ fails for every finite $3\le n<\omega$. This left $\omega^\omega$ (the first limit case beyond the failing finite powers) as the natural next test, and Erdős separately offered \$20 for pinning down exactly which finite-exponent cases fail (resolved by Specker himself). - The theorem: Chang, "A partition theorem for the complete graph on $\omega^\omega$," J. Combin. Theory Ser. A 12 (1972), 396–452 [Ch72], proved $\omega^\omega \to (\omega^\omega,3)^2$ — collecting Erdős's \$250. - Immediate generalization: E. C. Milner (unpublished, per erdosproblems.com/590) modified Chang's argument to show $\omega^\omega \to (\omega^\omega,m)^2$ for every finite $m$, not just $m=3$. - Shorter proof: Larson, "A short proof of a partition theorem for the ordinal $\omega^\omega$," Ann. Math. Logic 6(2) (1973/74), 129–145 [La73], reproved Milner's all-$m$ result with a cleaner argument (though, per the formalization literature, still technically demanding — "not actually a short proof" in absolute terms, only relative to Chang's original). - Machine-checked: Paulson (arXiv:2104.11613) and Džamonja–Koutsoukou-Argyraki–Paulson (arXiv:2011.13218, *Experimental Mathematics* 31:2 (2022) 383–400) formalized the full Erdős–Milner → Specker → Larson chain culminating in Milner's $\omega^\omega\to(\omega^\omega,m)^2$ in Isabelle/HOL (Archive of Formal Proofs, "Ordinal Partitions," Aug 2020). Along the way they had to re-derive and fix genuine errors in the original 1972 Erdős–Milner paper (a full-page corrigendum was needed, 1974) — a concrete example of formal verification catching mistakes that survived peer review and PhD examination for years. - Sibling/generalization problems on the same site: Erdős #591 — is $\omega^{\omega^2}\to(\omega^{\omega^2},3)^2$? (the next level up, $\omega^{\omega^2}\to(\omega^{\omega^2},3)^2$, resolved independently by Schipperus and Darby) and Erdős #592 — characterize the countable partition ordinals (open, \$1000: characterize *all* countable ordinals $\beta$ for which $\omega^\beta\to(\omega^\beta,3)^2$ — the "partition ordinals" problem, of which #590 is the $\beta=\omega$ instance).

Solution

Answer: TRUE. $\omega^\omega \to (\omega^\omega,3)^2$ — proved by Chang (1972); generalized to all finite $m$ by Milner and reproved more cleanly by Larson (1973).

The transferable technique — climb the ordinal tower by an inductive "step-up" lemma on indecomposable ordinals.

The proof machinery that makes results at the $\omega^\omega$ level tractable (and that is the reusable engine behind the whole ordinal-partition-calculus literature, including Larson's cleaner reproof of Milner's theorem) is a step-up theorem, established by Erdős and Milner and used repeatedly by Larson (arxiv.org/pdf/2104.11613, §4–5, full technical statement):

> If $\alpha$ is indecomposable (a power of $\omega$), $\alpha \to (k,\gamma)^2$ for some $k\ge2$, and $\beta$ is any countable ordinal, then > $$\alpha\cdot\beta \;\longrightarrow\; (2k,\ \min(\gamma,\omega^\beta))^2.$$

Read operationally, this is a machine for manufacturing a partition relation at ordinal-product scale $\alpha\cdot\beta$ out of one already known at the smaller scale $\alpha$, at the cost of (a) doubling the target size of the small-side homogeneous set ($k\to 2k$) and (b) capping the large-side homogeneous order type at $\omega^\beta$. The proof of the step-up lemma itself works by: 1. Writing the ordinal $\alpha\cdot\beta$ as a $\beta$-indexed sequence of $\alpha$-blocks, and using that every ordinal decomposes canonically (Cantor normal form) into a finite sum of indecomposable pieces, so the "obvious" partition of $\beta$ used to organize the induction can always be reduced to working with indecomposable chunks. 2. A key lemma about indecomposable ordinals: given any point $x$ inside a set $A$ of indecomposable order type $\alpha$, and any subset $A_1\subseteq A$, there is a subset $A_2\subseteq A_1$ of order type still $\alpha$ that lies entirely above $x$ — indecomposability is exactly what lets you "shrink and shift" a homogeneous witness without losing its order type. This is the combinatorial fact that makes transfinite recursive constructions of the homogeneous set well-founded. 3. An elaborate but finitary-flavored recursive construction of the eventual monochromatic set $Z$: enumerate $\beta$ with each element repeating infinitely often, and build an increasing family of candidate sets $A^{(n)}_\nu$ by complete induction on $n$, extracting one new point $x_n$ of $Z$ at each stage while re-partitioning the remaining ordinal into finitely many "clean" intervals around the points used so far (Erdős–Milner claims (8)–(10) in the original numbering; this is the part that both original papers got subtly wrong and that Paulson's formalization had to repair using the 1974 corrigendum).

**Why this is the transferable idea for the open problems downstream (Erdős #591 — is $\omega^{\omega^2}\to(\omega^{\omega^2},3)^2$?, Erdős #592 — characterize the countable partition ordinals):** the whole strategy for pushing partition relations up through $\omega^\omega, \omega^{\omega^2}, \omega^{\omega^\gamma},\dots$ is the *same* step-up-by-multiplication engine, iterated along the Cantor-normal-form decomposition of the target exponent, always paying the same currency (double the small side, cap the large side at a power of $\omega$). Every known positive result in the family — Chang at $\gamma=1$ (this problem), Schipperus/Darby at $\gamma=2$ (Erdős #591 — is $\omega^{\omega^2}\to(\omega^{\omega^2},3)^2$?), and Schipperus's general "$\gamma$ = sum of $\le2$ indecomposables" theorem toward Erdős #592 — characterize the countable partition ordinals — is a variant of this induction; every known negative result exploits the point where the induction's bookkeeping (the number of indecomposable summands you must chain through) breaks down. The frontier of #592 (exactly 3 indecomposable summands) is, in this light, precisely the point where nobody has yet found either (a) a way to make the step-up induction go one link further, or (b) a counterexample construction generalizing the ones that kill 4-or-more-summand cases. A derivation attack on #592 is thus naturally scoped as: extend or replace the Erdős–Milner/Larson step-up lemma so it survives one more level of the Cantor-normal-form chain.

Related

- Erdős #591 — is $\omega^{\omega^2}\to(\omega^{\omega^2},3)^2$? — the next rung: $\omega^{\omega^2}\to(\omega^{\omega^2},3)^2$, resolved independently by Schipperus and Darby using the same family of step-up/indecomposable-ordinal techniques. - Erdős #592 — characterize the countable partition ordinals — open (\$1000): characterize all countable ordinals $\beta$ with $\omega^\beta\to(\omega^\beta,3)^2$; #590 is exactly the $\beta=\omega$ (one indecomposable summand) instance of this general question, and its proof technique is the base case of the general attack. - Does the K3 partition-ordinal property imply the Kn property? (Erdős–Hajnal, disproved by Darby/Schipperus/Larson) — resolved-negative sibling: the $K_3$-partition-ordinal property does not imply the $K_n$-property for all finite $n$, via the same Schipperus/Darby counterexample machinery that bounds how far the step-up induction can be pushed. - Ordinal partition calculus — arrow notation $\\alpha\\to(\\alpha,m)^2$ and the self-partitioning-ordinal program — the general Erdős–Rado arrow-notation framework ($\alpha\to(\beta_0,\dots,\beta_{k-1})^n$) this problem lives in. - Additively indecomposable ordinals (Cantor's γ-numbers) — the ω^β / Cantor-normal-form-monomial ordinals — the powers of $\omega$; the necessary structural precondition for any $\alpha\to(\alpha,3)$ relation, and the building block the step-up lemma operates on. - Cantor normal form — decomposition of every ordinal into a strictly-decreasing sum of ω^β monomials — the canonical decomposition of an ordinal into indecomposable summands; the axis along which the step-up induction is organized and along which the open #592 frontier (1–2 vs. 3 vs. ≥4 summands) is stated. - Topological Ramsey spaces / Nash-Williams tree-front machinery — Nash-Williams-style tree/front machinery underlying the more modern reformulations of these arguments (used in Larson's and later proofs in this family). - Machine formalization of infinitary combinatorics proofs (Isabelle/HOL, Lean) — Paulson et al.'s Isabelle/HOL formalization of the full Specker→Chang→Erdős-Milner→Larson chain (arXiv:2011.13218, arXiv:2104.11613), notable for having caught and fixed genuine errors in the 1972 published proof via the 1974 corrigendum.