Erdős Problem a Daythe open tracker

Erdős Problem #23

FALSIFIABLEdatabase updated 2025-08-31

Still open — but if it is false, a finite counterexample exists, so a computer search could in principle disprove it. A search can't prove it.

What the community database records, not our verdict. erdosproblems.com no longer shows statuses (why).

The blow-up of the 5-cycle \(C_5\): replace each vertex of \(C_5\) with an independent set of \(n\) vertices, and connect two vertices iff their corresponding vertices in \(C_5\) are adjacent. The vertex set is \(\mathbb{Z}/5\mathbb{Z} \times \{0, \ldots, n-1\}\), where \((i, a)\) and \((j, b)\) are adjacent iff \(j = i + 1\) or \(i = j + 1\) in \(\mathbb{Z}/5\mathbb{Z}\).

Can every triangle-free graph on \(5n\) vertices be made bipartite by deleting at most \(n^2\) edges?
Statement as formalized in Formal Conjectures (Google DeepMind, Apache-2.0) · their label: research open · 2 further variants / known partial results in the Lean file. The authoritative wording is on erdosproblems.com/23.
Prizenone
Topicsgraph theory
Statement in LeanFormal Conjectures
Solution in Leanno
OEISA389646
Original pageerdosproblems.com/23
EARLY RUN BY THIS SITE · JUL 25, 2026

No counterexample found — search exhausted its budget. Problem open.

WALL