Erdős Problem #128
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).
Attempts
submit one →Read our full write-up →
The $250 sparse-halves problem asks whether every triangle-free graph has ⌊n/2⌋ vertices spanning at most n²/50 edges; Razborov's 27/1024 (2021) is the best bound in print. The proof-claims tab carries one claim: Amir Sarid (Aug 2026), β ≤ 131/5000 = 0.0262, conditional on Balogh–Clemen–Lidický's max-cut Theorem 2(a), with a Lean development taking that theorem as a hypothesis. We refereed it: every lemma recomputed by hand and by a second route (exact rationals, randomised tests with mutation controls), the C₄ flag certificate re-established by an independent exact verifier and probed on 14,651 small graphs, the Lean source audited and then kernel-replayed on our box (Mathlib v4.30.0, standard axioms only, statement match, sorry and wrong-shape negative controls). Verdict: HOLDS AS READ, label (b) — but the theorem it rests on is a six-page EuroComb 2021 extended abstract whose proof sketch does not separately cover the part he uses, with no public certificate, so the unconditional record stays 27/1024. Not ours; the problem stays open. Also: two errors on the live problem page, staged for Patrick.
LIVE