Claims

../

1972_05_01_chang: Chang proves ω^ω → (ω^ω, 3)^2, that every red-blue coloring of the pairs from the ordinal ω^ω has a red set of order type ω^ω or a blue triangle, the statement of Problem 590, in a 57-page paper of 1972.

1973_12_01_larson: Larson proves ω^ω → (ω^ω, m)^2 for every finite m by a short argument; the case m = 3 is the statement of Problem 590, and the Lean formalization in Boris Alexeev's repository follows her proof.

---