Erdős Problem a Daythe open tracker

Erdős Problem #621

PROVED LEANdatabase updated 2026-04-19

The statement as posed is true, and a proof exists. A solution has also been checked by machine, in Lean.

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

Let \(G\) be a graph on \(n\) vertices, \(\alpha_1(G)\) be the maximum number of edges that contain at most one edge from every triangle, and \(\tau_1(G)\) be the minimum number of edges that contain at least one edge from every triangle. Is it true that\[\alpha_1(G)+\tau_1(G) \leq \frac{n^2}{4}?\] A problem of Erdős, Gallai, and Tuza [EGT96], who observe that this is probably quite difficult since there are different examples where equality hold: the complete graph, the complete bipartite graph, and the graph obtained from \(K_{m,m}\) by adding one vertex joined to every other. This is true, and was proved by Norin and Sun [NoSu16], who in fact proved that\[\alpha_1(G)+\tau_B(G) \leq \frac{n^2}{4},\]where \(\tau_B(G)\) is the minimum number of edges that need to be removed to make the graph bipartite. Here \(\alpha_1(G)\) and \(\tau_1(G)\) are taken over subsets of the edge set of \(G\), and the inequality is stated multiplied through by \(4\) so that it lives in the natural numbers. The linked file states \(\tau_1\) as the least number of edges whose deletion leaves \(G\) triangle-free, which is the same as meeting every triangle of \(G\), and quantifies over an arbitrary `Fintype V` rather than `Fin n`.
Statement as formalized in Formal Conjectures (Google DeepMind, Apache-2.0) · their label: research solved. The authoritative wording is on erdosproblems.com/621.
Prizenone
Topicsgraph theory
Statement in LeanFormal Conjectures
Solution in Leanyes
Original pageerdosproblems.com/621
NOBODY HAS SENT US AN ATTEMPT YET

If you take a run at this one — with your own AI subscription or without — the guide says how, and the submission form gets you an honest read of what you found.