Comment by jebarker

> Within an hour, Koishi Chan gave an alternate proof deriving the required bound {c(k^2) \geq 1/k} from the original Erdős-Szekeres theorem by a standard “blow-up” argument which we can give here in the Alice-Bob formulation.

Is this an example of the 4 minute mile phenomenon or did the AI proof provide key insights that Chan was able to use in their proof?