Erdős Problem 591

Reference: erdosproblems.com/591

theorem erdos_591 : OmegaPowerRamsey (Ordinal.omega0 ^ 2) 3 ↔ sorry

Let $α$ be the infinite ordinal $\omega^{\omega^2}$. Is it true that any red/blue colouring of the edges of $K_α$ there is either a red $K_α$ or a blue $K_3$.