---

Claim. $\omega^\omega\to(\omega^\omega,3)^2$: in every red/blue coloring of the edges of $K_\alpha$ with $\alpha=\omega^\omega$ there is a red $K_\alpha$ or a blue $K_3$ (the Theorem, p. 396; which color carries the triangle is a convention, and the paper puts it the other way round). This is the question of Problem 590, which the paper records as Problem 7 of the Erdős–Hajnal list. The proof is by induction from the Normal Form, Super Form, Transitivity and Well-Foundedness Lemmas (pp. 403–405), using Erdős's relation $\omega^{2n+1}\to(\omega^{n+1},4)^2$; the author calls it long and complicated.

Source. C. C. Chang, A partition theorem for the complete graph on $\omega^\omega$, J. Combinatorial Theory Ser. A 12 (1972), no. 3, 396–452, received 1970-02-24, issue dated May 1972; this page is dated by the issue month, since the issue prints no day. The Theorem, the lemma statements and the proof of the Theorem from the lemmas are the basis of this page, recorded on the source card and its theorem page; the proofs of the lemmas are followed for structure only and nothing is independently reviewed. Footnote 1 (p. 397) reports Milner's extension $\omega^\omega\to(\omega^\omega,m)^2$ for every finite $m$, communicated by letter without a printed proof, which is disclosed here rather than given a page, and Larson's shorter proof of both results in her 1972 Dartmouth thesis, published in 1973 and recorded on Larson's claim page.

Acceptance. Refereed: the Journal of Combinatorial Theory, Series A. Reviewed: the curator of erdosproblems.com (T. F. Bloom) labels the problem PROVED (LEAN) and credits Chang [Ch72] with the proof in the problem's commentary, with Milner's extension and Larson's shorter proof noted. The curator is independent of the author.

Formalization. formal-conjectures 590.lean (2026-10-07) marks its statement erdos_590 research solved with a formal-proof link to Erdos590.lean in Boris Alexeev's repository at the pinned commit. That file declares itself a Lean formalization of a solution to Problem 590, names Chang and Larson as its informal authors and Codex and GPT-5.6 Sol as its formal authors, follows Larson's proof of the stronger theorem for every finite $m$, and states the theorem as OrdinalCardinalRamsey (ω ^ ω) (ω ^ ω) 3, the namespace and type of the formal-conjectures specification. It is not built here, so it is a link and not formalized evidence.