---

Claim. $\omega^\omega\to(\omega^\omega,m)^2$ for every finite $m$: 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_m$. The case $m=3$ is the question of Problem 590, first proved by Chang (Chang 1972); the theorem for every finite $m$ is the extension that Chang's footnote 1 (p. 397) reports Milner as having communicated by letter without a printed proof. Larson's paper gives a shorter proof of both, as Chang's footnote 1 reports, so it is a second proof of the problem's statement and has its own page.

Source. J. A. Larson, A short proof of a partition theorem for the ordinal $\omega^\omega$, Ann. Math. Logic 6 (1973), no. 2, 129–145, doi:10.1016/0003-4843(73)90006-5; the issue is dated December 1973, and this page is dated by the issue month, since the issue prints no day. Chang's footnote places the proof in Larson's 1972 Dartmouth thesis. The paper is not held: the statement is recorded from the publisher's record, Chang's footnote and the site's commentary, and nothing is independently reviewed.

Acceptance. Refereed: Annals of Mathematical Logic. Reviewed: the curator of erdosproblems.com (T. F. Bloom) labels the problem PROVED (LEAN) and credits Larson [La73] with the shorter proof in the problem's commentary. The curator is independent of the author.

Formalization. Erdos590.lean in Boris Alexeev's repository, linked above at its pinned commit, 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, and says that its combinatorics follows Larson's proof of the stronger theorem for every finite $m$. It states the theorem as OrdinalCardinalRamsey (ω ^ ω) (ω ^ ω) 3, the namespace and type of the formal-conjectures specification, which formal-conjectures 590.lean (2026-10-07) marks research solved with a formal-proof link to that file. The file is not built here, so it is a link and not formalized evidence.