Erdős Problem a Daythe open tracker

Erdős Problem #1010

PROVEDdatabase updated 2025-09-10

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).

Let \(t<\lfloor n/2\rfloor\). Does every graph on \(n\) vertices with \(\lfloor n^2/4\rfloor+t\) edges contain at least \(t\lfloor n/2\rfloor\) triangles? Rademacher proved that every graph on \(n\) vertices with \(\lfloor n^2/4\rfloor+1\) edges contains at least \(\lfloor n/2\rfloor\) triangles. Erdős [Er62d] proved that every graph on \(n\) vertices with \(\lfloor n^2/4\rfloor+t\) edges contains at least \(t\lfloor n/2\rfloor\) triangles, for all \(t<cn\), for some constant \(c>0\). This is true, and was proved independently by Lovász and Simonovits [LoSi76] and Nikiforov and Khadzhiivanov [NiKh81].
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/1010.
Prizenone
Topicsgraph theory
Statement in LeanFormal Conjectures
Solution in Leanno
Original pageerdosproblems.com/1010
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.