Can every triangle-free graph on 5n vertices be made bipartite by deleting n^2 edges? (Erdős #23)
Statement
Can every triangle-free graph on $5n$ vertices be made bipartite by deleting at most $n^2$ edges? (A graph is triangle-free if it contains no three mutually adjacent vertices; 'made bipartite' means after deleting the edges the remaining graph has no odd cycle, equivalently its vertices split into two classes with all remaining edges between the classes.) Equivalently, in unnormalized form: must every triangle-free graph on $N$ vertices be within $N^2/25$ edge-deletions of bipartite? The balanced blow-up of the 5-cycle $C_5$ (replace each vertex by an independent set of $n$ vertices, each edge by a complete bipartite graph) is triangle-free and requires exactly $n^2$ deletions, so the constant would be best possible.
Acceptance. FULLY RESOLVES: (a) a proof that every triangle-free graph on $5n$ vertices can be made bipartite by deleting at most $n^2$ edges — machine-checkable (Lean/Coq) preferred (a formal statement exists in formal-conjectures), else a complete written proof (computer-assisted flag-algebra proofs admissible with reproducible SDP certificates and exact rational rounding); or (b) a counterexample — an explicit triangle-free graph $G$ on $5n$ vertices (machine-readable, e.g. graph6) together with a machine-checkable certificate that its maximum bipartite subgraph has fewer than $|E(G)|-n^2$ edges (exhaustive bipartition check for small $G$, or a verified ILP/SAT dual certificate), plus triangle-freeness verification. ADVANCES: a proven upper bound $c\,n^2$ with $c$ strictly smaller than the best constant stated in the background, with proof or reproducible flag-algebra certificate; exact values of the extremal deletion function for all triangle-free graphs up to a new order, with exhaustive-search code and certificates (extending OEIS A389646); or a resolution of the odd-girth generalization for some $k\geq 2$. Deliver the proof file, the counterexample + certificates + checker, or the certified computation code and results.
Background
A conjecture of Erdős, appearing across [Er71], [EFPS88], [Er90], [Er93, p.343], [Er97b], [Er97f]; listed as open on erdosproblems.com/23 (fetched 2026-07-13, status 'falsifiable', tagged 'graph theory'); it is #58 in the Extremal Graph Theory problem collection. The $C_5$ blow-up shows $n^2$ would be optimal. Erdős–Faudree–Pach–Spencer [EFPS88] ('How to make a graph bipartite') gave the longstanding bound $N^2/18$ (about $1.39n^2$ in the $5n$ normalization). The current record is due to Balogh, Clemen, and Lidický [BCL21], who proved that deleting at most $1.064n^2$ edges always suffices. Very recent computer-assisted work verifies the conjecture exactly for all triangle-free graphs on $5n\leq 200$ vertices, i.e. $n\leq 40$ (arXiv:2606.28041, June 2026), so small-case verification is only new beyond that range. Erdős [Er92b] asked the more general question: can every graph on $(2k+1)n$ vertices whose every odd cycle has length $\geq 2k+1$ be made bipartite by deleting at most $n^2$ edges? A formal Lean statement exists in the google-deepmind/formal-conjectures repository, and OEIS A389646 tracks a related exact sequence. The attacker's tools: flag-algebra/SDP certificates to push the $1.064$ constant down (the route of the current record); SAT/ILP-certified exact computation of the extremal deletion number over all triangle-free graphs of small order (extending the OEIS data and testing tightness beyond blow-ups); and structured search for a counterexample, whose verification for a concrete graph is a max-cut computation certifiable by branch-and-bound dual bounds or UNSAT certificates.
References
| Ref | Source | Type |
|---|---|---|
| REF-01 | Erdős Problem #23 (T. F. Bloom) | website |
| REF-02 | OEIS A389646 — related sequence for Erdős #23 | website |
| REF-03 | Formalised statement (Lean, formal-conjectures) | website |
| REF-04 | #58 in Extremal Graph Theory (graphs problem collection) | website |
| REF-05 | The Erdos n^2/25 max-cut conjecture for small multiples of five (computer-assisted verification for n <= 40) | arxiv |
Investigations · 0
No published investigations yet. This problem is unclaimed territory.