PROVED (LEAN). Theorem 2.1 of Conlon, Fox and Sudakov [CFS14b] gives, for every $r\ge2$, a $K_{r,r}$-free subgraph with at least $\tfrac14m^{r/(r+1)}$ edges in every graph with $m$ edges; at $r=2$, $K_{2,2}=C_4$ and the bound is $\tfrac14m^{2/3}$, the statement with $c=\tfrac14$. Their Theorem 2.3 at $r=s=2$ shows the order is tight: the complete bipartite graph with parts of sizes $m^{1/3}$ and $m^{2/3}$ has $m$ edges and no $C_4$-free subgraph with more than $2m^{2/3}$ edges. The status-defining source is an arXiv note (v1, 27 January 2014); the site accepted it, a forum proof of the same bound with $c=\tfrac12$ stands in the thread, and an external Lean proof of the bound with $c=\tfrac12$ accompanies the site's label (both recorded below, neither taken as the page's own). The thread also reports that the result reappears as Theorem 3.1 of the same authors' refereed paper Short proofs of some extremal results II (J. Combin. Theory Ser. B 121 (2016), 173--196), whose arXiv v2 states it as Theorem 3.1, quoted below; the journal text was not compared. The claim pages Conlon, Fox and Sudakov 2014 and Hunter's forum proof of 2025 record the two results, their postings and the acceptance evidence; the Lean development of 2026 described under Formalization names both as the informal authors of what it proves and is a formalization link on both pages, not a claim of its own. A third page, Aristotle's proof with c equal to three eighths, records a pending claim: a Lean proof of the bound with $c=\tfrac38$ that the same development's author committed on 20 January 2026 and announced in an update to his comment of 17 January 2026, and that names no informal author, found by the automated prover Aristotle from the statement alone. The standing in the frontmatter is derived from the three pages.