Is $\omega_1^2\not\to(\omega_1^2,k)^2$ provable in ZFC for every finite $k$? (Erdős #1169)

Write $\alpha\to(\beta,\gamma)^2$ for the partition relation asserting that every $2$-colouring $c:[\alpha]^2\to\{0,1\}$ of the unordered pairs from an ordinal $\alpha$ yields either a $0$-homogeneous subset of order type $\beta$ or a $1$-homogeneous subset of order type $\gamma$; $\not\to$ is its negation. Let $\omega_1^2$ denote the ordinal $\omega_1\cdot\omega_1$. Is it true that, for every finite $k<\omega$, $$\omega_1^2\not\to(\omega_1^2,k)^2\,?$$ The site displays the base case $k=3$: is there a $2$-colouring of $[\omega_1^2]^2$ — equivalently a graph on $\omega_1^2$ whose edges are the $1$-coloured pairs — that is triangle-free (no $1$-homogeneous triple) yet contains no $0$-homogeneous (independent) set of order type $\omega_1^2$?

Acceptance. FULLY RESOLVES: a complete proof — machine-checkable (Lean/Coq) preferred, else a full written proof — that settles the relation in ZFC, i.e. either that $\omega_1^2\not\to(\omega_1^2,k)^2$ holds for every finite $k<\omega$, or that it fails for some finite $k$; OR a proof that the statement is independent of ZFC, exhibiting both a model where it holds (Hajnal's CH model covers one direction) and a forcing/inner model where it fails. ADVANCES (each itself checkable): prove the relation under a hypothesis strictly weaker than the best one currently known to suffice — stated in words, that hypothesis is the continuum hypothesis (Hajnal), so require a strictly weaker set-theoretic assumption with full proof; OR settle a specific finite $k$ outright in ZFC; OR construct a forcing model in which the relation provably fails; OR deliver a Lean/Coq formalization of Hajnal's CH proof. Deliver the proof object or a complete manuscript giving the colouring/forcing construction.