Claims

../

2014_01_27_conlon_fox_sudakov: Theorem 2.1 of Conlon, Fox and Sudakov (arXiv 2014; Theorem 3.1 of their refereed paper in J. Combin. Theory Ser. B 2016) gives every graph with m edges a C_4-free subgraph with at least a quarter of m^{2/3} edges; accepted.

2025_09_13_zach_hunter: A forum thread post of 13 September 2025 proves that every graph with m edges has a C_4-free subgraph with at least half of m^{2/3} edges, by the deletion method with a sharper four-cycle count; accepted on review.

2026_01_20_alexeev: A Lean proof, committed by Boris Alexeev on 20 January 2026, that every graph with m edges has a C_4-free subgraph with at least three eighths of m^{2/3} edges; found by the automated prover Aristotle from the statement alone.

---