SOLVED - $250
Prove that
\[R(4,k) \gg \frac{k^3}{(\log k)^{O(1)}}.\]
Spencer
[Sp77] proved
\[R(4,k) \gg (k\log k)^{5/2}.\]
Ajtai, Komlós, and Szemerédi
[AKS80] proved
\[R(4,k) \ll \frac{k^3}{(\log k)^2}.\]
This is true, and was proved by Mattheus and Verstraete
[MaVe23], who showed that
\[R(4,k) \gg \frac{k^3}{(\log k)^4}.\]
This problem is #5 in Ramsey Theory in the graphs problem collection.