Erdős Problem #1080

Let \(G\) be a bipartite graph on \(n\) vertices such that one part has \(\lfloor n^{2/3}\rfloor\) vertices. Is there a constant \(c>0\) such that if \(G\) has at least \(cn\) edges then \(G\) must contain a \(C_6\)? The answer is no, as shown by De Caen and Székely [DeSz92], who in fact show a stronger result. Let \(f(n,m)\) be the maximum number of edges of a bipartite graph between \(n\) and \(m\) vertices which does not contain either a \(C_4\) or \(C_6\). A positive answer to this question would then imply \(f(n,\lfloor n^{2/3}\rfloor)\ll n\). De Caen and Székely prove \(n^{10/9}\gg f(n,\lfloor n^{2/3}\rfloor) \gg n^{58/57+o(1)}\) for \(m\sim n^{2/3}\). They also prove more generally that, for \(n^{1/2}\leq m\leq n\), \(f(n,m) \ll (nm)^{2/3},\) which was also proved by Faudree and Simonovits. This was formalized in Lean by Alexeev using Aristotle.