Erdős problem 1128

Explicit form of Prikry–Mills:

There exists a 2-colouring of $\omega_1 \times \omega_1 \times \omega_1$ such that for every countably infinite $A_1, B_1, C_1 \subseteq \omega_1$, the box $A_1 \times B_1 \times C_1$ is not monochromatic.

This is the content of the Prikry–Mills theorem (1978, unpublished), stated using Lean's ordinal type {o : Ordinal // o < ω_ 1} as the representation of $\omega_1$.