The board / graph theory / #88
Erdős Problem #88
PROVEDdatabase updated 2025-08-31
The statement as posed is true, and a proof exists.
What the community database records, not our verdict. erdosproblems.com no longer shows statuses (why).
For any \(\epsilon>0\) there exists \(\delta=\delta(\epsilon)>0\) such that if \(G\) is a graph on \(n\) vertices with no independent set or clique of size \(\geq \epsilon\log n\) then \(G\) contains an induced subgraph with \(m\) edges for all \(m\leq \delta n^2\). This was conjectured by Erdős and McKay and proved by Kwan, Sah, Sauermann, and Sawhney [KSSS22]. Erdős' original formulation also assumed that \(G\) has \(\gg n^2\) edges. By an old result of Erdős and Szemerédi this follows from the other condition, so it is omitted here.
Statement as formalized in Formal Conjectures (Google DeepMind, Apache-2.0) · their label: research solved · 2 further variants / known partial results in the Lean file. The authoritative wording is on erdosproblems.com/88.Prize$100
Topicsgraph theory, ramsey theory
Statement in LeanFormal Conjectures
Solution in Leanno
Original pageerdosproblems.com/88
Attempts
submit one →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.