Erdős Problem a Daythe open tracker

Erdős Problem #1092

DISPROVED LEANdatabase updated 2026-08-23

The statement as posed is false. 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).

An edge-budget function \(g\) is *admissible* for \(r\) if every graph \(G\) with the property that every subgraph \(H\) on \(m\) vertices is the union of a graph with chromatic number \(\leq r\) and a graph with \(\leq g(m)\) edges has chromatic number \(\leq r+1\). The quantification is over all finite graphs \(G\) (of any size), not just graphs on a fixed vertex set, and the condition on subgraphs is imposed at every size \(m\) simultaneously. The function \(f_r\) of the source is "maximal" among admissible functi

Is it true that \(f_2(n) \gg n\)? Disproved by Rödl, who showed \(f_r(n) = o(n)\) for all fixed \(r \geq 2\). A conjecture of Erdős, Hajnal, and Szemerédi. This seems to be closely related to, but distinct from, [744](https://www.erdosproblems.com/744). Tang notes in the comments that Rödl [Ro82] constructed, for any \(\epsilon>0\) and \(k\), a graph with chromatic number \(\geq k\) such that every graph on \(m\) vertices is bipartite after deleting at most \(\epsilon m\) edges.
Statement as formalized in Formal Conjectures (Google DeepMind, Apache-2.0) · their label: research solved · 1 further variant / known partial result in the Lean file. The authoritative wording is on erdosproblems.com/1092.
Prizenone
Topicschromatic number, graph theory
Statement in LeanFormal Conjectures
Solution in Leanyes
Original pageerdosproblems.com/1092
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.