---

Claim. The answer to Problem 1008 is yes, with $c=\tfrac38$: every graph $G$ with $m$ edges contains a $C_4$-free subgraph with at least $\tfrac38m^{2/3}$ edges. The claim is a Lean proof, the file src/v4.24.0/ErdosProblems/Erdos1008b.lean of Boris Alexeev's repository plby/lean-proofs, first committed on 20 January 2026 and announced in an undated update, made no earlier than that commit, to Alexeev's comment of 17 January 2026 reporting the formalization of Conlon, Fox and Sudakov's proof: the update says that Aristotle, the automated prover of Harmonic, proved the result by itself given only the statement and obtained the constant $\tfrac38$. The claimant is Alexeev, who posted the result; the prover is Aristotle, named as the update names it. The file's header describes the argument: the number of $4$-cycles is bounded by $m^2$ through a count of disjoint edge pairs, and a probabilistic deletion argument then finds a large $C_4$-free subgraph. It is the deletion method of Conlon, Fox and Sudakov and of Hunter with a weaker count of $4$-cycles than Hunter's $\binom m2$, hence the constant between their $\tfrac14$ and $\tfrac12$.

Submission note. Posted to the site's forum by Boris Alexeev on 17 January 2026:

The proof by Conlon & Fox & Sudakov [CFS14b] was formalized, giving the explicit result that every graph with $m$ edges contains a subgraph with $\frac{15}{32} m^{2/3}$ edges which contains no $C_4$. Type-check it online!

It occurs to me now, after the fact, that perhaps Aristotle could prove this result by itself given only the statement. I'll give it a try.

Update: Aristotle was able to prove the result by itself given only the statement. It got the constant $\frac{3}{8}$.

Update #2: Aristotle was able to prove the constant $\frac{1}{2}$ (as in Zach Hunter's comment) given only the formal statement. That's probably the best proof of the three linked in this comment.

(The site has been updated to address this comment.)

The development. The file at the pinned commit (1,020 lines; import Mathlib its only import) names no informal or formal author in a header: it opens with the one-paragraph description above and a namespace Erdos1008b. Its final theorem, exists_C4_free_subgraph_with_many_edges, states that every finite simple graph $G$ has a set $S'$ of its edges no four of which form a $4$-cycle (the file's own is_C4: a $4$-set of edges whose graph contains cycleGraph 4) with $|S'|\ge\tfrac38|E(G)|^{2/3}$. The file has no sorry and no axiom; native_decide occurs once, in the lemma cycleGraph4_disjoint_pairs_card, which no later declaration of the file names, so the final theorem does not appear to depend on it, though the file prints no #print axioms output. The step from the file's theorem to the formal-conjectures statement of the problem (the subgraph on the edge set $S'$ is $C_4$-free and $\le G$; $c=\tfrac38$) is in neither file. The post's second update reports that Aristotle also proved the constant $\tfrac12$ given only the formal statement (Erdos1008c.lean under the same sources); the repository's consolidated file with that constant names Conlon, Fox, Sudakov, Hunter and ChatGPT as informal authors and is recorded as a formalization link on their pages, not as a claim.

Depends on. No page of this wiki; the file is self-contained over Mathlib.

Standing. Claimed. No build, audit or kernel check of the file exists in this corpus, and no outside examination of it is published, so the page lists no formalized evidence. The site's label PROVED (LEAN) and the community database's record rest on the results of Conlon, Fox and Sudakov and of Hunter and on the consolidated development with $c=\tfrac12$; neither names this proof, and the problem's standing does not rest on it.