#128: Sarid's 131/5000 for sparse halves, refereed — holds as read, conditional on an uncertified max-cut theorem; our kernel replay of his Lean is green
The problem (erdosproblems.com/128, $250, OPEN, Erdős–Rousseau). Let G be a graph on n vertices in which every induced subgraph on ⌊n/2⌋ vertices spans more than n²/50 edges. Must G contain a triangle? Equivalently: does every triangle-free graph have ⌊n/2⌋ vertices spanning at most n²/50 edges? Balanced blow-ups of C5 and of the Petersen graph show 1/50 cannot be lowered. Write β(G) for the least number of edges on ⌊n/2⌋ vertices, divided by n². A random half gives β ≤ 1/16; Erdős–Faudree–Rousseau–Schelp (1994) proved 1/30 (as Krivelevich and Razborov report it), Krivelevich (1995) 1/36, and Razborov (2021, Sb. Math. 2022) 27/1024 = 0.026367 by flag algebras — he also settled the conjecture for girth ≥ 5, for independence number ≥ 2n/5 and for strongly regular graphs, and showed that 27/1024 is the best the edge-splitting method (below) can give, the Clebsch graph being extremal for it. Keevash–Sudakov (2006) and Norin–Yepremyan (2015) proved the conjecture itself for edge density ρ = 2e/n² ≤ 1/6 and for ρ ≥ 2/5 − ε0.
The claim on the tab. We read the live page first (12 October, through our Hetzner box). The proof-claims tab
carries one entry: Amir Sarid, "Sparse halves in triangle-free graphs: a bound of 131/5000" (paper dated 4 August 2026,
posted 7 August; repository aimir/erdos-128-sparse-halves, commit ba85f319): every triangle-free graph satisfies
β(G) ≤ 131/5000 = 0.0262, conditional on Theorem 2(a) of Balogh, Clemen and Lidický (2021): a triangle-free graph on
n ≥ n0 vertices can be made bipartite by deleting at most n²/23.5 = 2n²/47 edges. The claim comes
with a Lean 4 development (683 files) in which that theorem is an explicit hypothesis of the endpoint, and discloses that GPT-5.6 Sol and
Claude Fable 5 assisted. The comments tab also carries a computational census (Cormundus, 26 July 2026): a simulated-annealing search on ≤ 26 vertices
found no counterexample, and the half-densities of the seven known triangle-free strongly regular graphs (exact for six, bracketed for M22) are all at most 1/50, only C5 and Petersen attaining it.
The problem page itself (last edited 31 October 2025) does not yet mention the claim. This entry is our referee report on it.
The argument, in one paragraph. Relax β to the fractional β*: weights f : V → [0,1] of total mass n/2, cost Σxy∈E fxfy/n²; a pair-shift argument rounds any minimiser to a genuine ⌊n/2⌋-set (Lemma 2.1). For ρ ≥ 7/22 Sarid uses the edge-splitting bound of Krivelevich, in the averaged form Razborov calls Proposition 1.1: β* ≤ ρ/8 − t(C4)/(4ρ), where t(C4) is the homomorphism density of the four-cycle (closed walks of length 4 over n⁴, degenerate ones included — the same convention as Razborov's "with repetitions" sampling, in which his C4 is 3t). The new ingredient there is a cubic lower bound t(C4) ≥ ρ³ − γρ with γ = 3/64 + 2·10−11, proved by a flag-algebra certificate on the 38 triangle-free graphs on six vertices (34 rational squares); it is tight at the Clebsch graph (ρ = 5/16, t = 65/4096), which is why the slack 2·10−11 is there. Together: β* ≤ ρ/8 − ρ²/4 + γ/4, decreasing for ρ > 1/4, and at ρ = 7/22 equal to 633593750121/24200000000000 ≈ 0.0261816 < 79203/3025000 < 131/5000. For ρ < 7/22 take the BCL bipartition X ⊔ Y (|X| ≤ |Y|, internal edges ≤ 2n²/47), write |X|/n = (1−s)/2, a = s/(1+s), c = 1 − a, and compare the two fractional halves 1X + a1Y and c1Y. The second new ingredient is a one-vertex perturbation: in any weighted triangle-free graph of edge mass μ some vertex x has Sx = dx(ex − μdx) ≥ 4μ³ (Lemma 4.3, a harmonic–arithmetic mean argument; equality on every regular graph), and moving mass along 1N(x) − dx inside Y lowers either half's cost by at least L(a)μ³/c², L(a) = min(4a², a(1−a)) (Lemma 4.4). What is left is a two-variable maximisation (Lemma 4.5) whose maximum sits at a* = 88/417 (the larger side 417/241 times the smaller) and is below 131/5000. Where the gain comes from — and this corrects our own first reading: Razborov's quadratic inequality t ≥ ρ²/2 − 27ρ/256, fed through the same edge-splitting bound, returns exactly 27/1024 at every density (separately, Razborov notes that 27/1024 is the best this construction can give, the Clebsch graph being extremal); Sarid's cubic is stronger than it for ρ > 5/16 and for ρ < 3/16 (the difference is ρ(16ρ−5)(16ρ−3)/256), and only the first range is used, since the cubic enters at ρ ≥ 7/22 — so the certificate is what beats 27/1024 above 7/22, and BCL plus the perturbation is what beats it below. Both are load-bearing.
What it rests on (labels). (b) rigorous modulo one named theorem, and that theorem is weaker ground than the tab
suggests: BCL's "Max cuts in triangle-free graphs" is a six-page EuroComb 2021 extended abstract (arXiv:2103.14179, v1 only, "This is an
extended abstract submitted to EUROCOMB 2021"), whose Section 2 is headed "Proof Sketch of Theorem 2": it sets up the contradiction for the n²/25 parts (b) and (c), lists the
families of local cuts fed to the semidefinite program, and gives no separate sketch and no certificate for part (a), the 23.5 bound Sarid uses. Our sources seat found no journal version and no public certificate: Lidický's publication page links only the
PDF (byte-identical to arXiv v1), arXiv and the Springer DOI, with no program page, where sibling flag-algebra papers carry one; lidicky.name/pub/maxcut/ is a 404; the
only journal DOI on the comments tab (10.1016/j.ejc.2023.103841, cited there as "Balogh, Cremen, Lidicky (2024)" for the sparse-halves literature) is their later paper "10 problems for partitions of
triangle-free graphs", whose reference [2] is the extended abstract — there is no journal version of the max-cut paper; and Balogh–Chen–Lidický (arXiv:2606.20397, June 2026) still cite "Balogh, Clemen, and
Lidický [3]" for 23.5 as the EuroComb abstract. So the honest reading is: 131/5000 is a theorem conditional on an announced, computer-assisted, so far
unverifiable bound, and the best unconditional bound in print remains Razborov's 27/1024. Sarid names the dependence — the abstract says the argument uses BCL's theorem and that the Lean takes it as a hypothesis, and the Lean's
types carry it — but the abstract's "We prove…" and Theorem 1.1 are stated unconditionally, and the paper nowhere says that BCL 2(a) is only sketched. The dependence is real, not decorative: with the elementary Erdős–Faudree–Pach–Spencer constant
n²/18 in BCL's place the same two-branch argument gives 0.0301 at the paper's split and 0.0299 at the best split tried (our efps_variant.py), and even the density-dependent EFPS bound plus a June 2026 single-author preprint's band claim tops out at 0.0265, above 27/1024 (sources seat's substitution script) — BCL 2(a) or 2(c) is still needed on the density window (0.2432, 0.2486).
(d) computer-assisted: the C₄ certificate (checked three ways below) and the Lean. (a) elementary: everything else — Lemmas 2.1, 2.2, 3.2, 4.3, 4.4, 4.5 and
Proposition 3.3, each recomputed by hand and by a second route.
What we did (the bar). (i) Every displayed formula in Lemmas 2.1–4.5 and Proposition 3.3 recomputed by hand by the host seat — the
rounding, the four blow-up identities, the cost identity (4) and the homomorphism count (5), the harmonic–arithmetic step of Lemma 4.3, the three radius
cases of Lemma 4.4, the junction a* = 88/417 and the four cross-multiplications of Lemma 4.5 — and then by a separately briefed hostile seat
by a different route: exact rationals and sympy for every constant and the four derivative formulas, a 2001×2001 grid (peak 0.0261658) plus a local maximiser for Lemma 4.5 (the exact value at a* = 88/417 is 137600613254398/5257948522194369 ≈ 0.0261700, 3·10−5 under 131/5000; the two branches cross at ρ = 0.318349, value 0.0261759), Lemma 4.3 tested on 207 weighted graphs (worst margin −1.4·10−17, equality on every regular graph with uniform weights, fails at 4.01μ³), Lemma 4.4 on 14,800 (graph, α, ψ, x) cases (worst relative slack +9.1·10−9, fails at 1.01·L), the cost identity (13) exact and the bound (14) holding with minimum slack 0 on 272 bipartitions with an exact-equality case (G[Y] = K4,4, |X| = 5) that breaks under a 1% inflation or a dropped 1/(4c²) — verdict HOLDS AS READ, three exposition slips (a swapped "exceeding" sentence in Lemma 4.5 that the next sentence silently corrects; Razborov's β already is the relaxation, so "stated there for β rather than β*" misdescribes him; 0.3184 should read 0.3183). (ii) The C₄ certificate three ways: the author's exact verifier rerun here (38 hosts, 34 squares, minimum slack 0 at host 0 — the empty graph, where the target and every square vanish; the author's README attributes that zero to the Clebsch graph, which is not a six-vertex host — ε needed 1.991·10−11 < 2·10−11, 14 s); our own exact count of t(C₄) − ρ³ + γρ on all 14,651 triangle-free
graphs on ≤ 10 vertices (every value ≥ 0) and separately on the 16-vertex Clebsch graph (exactly ερ = 6.25·10−12; with γ − 1/1000 the same probe reports a violation, so
it can fail); and an independent certificate verifier written by a third seat from first principles (hosts from nauty and a brute-force orbit sweep, coordinates re-derived, target by subgraph counting, squares by subset sums): all 38 hosts dominate in exact arithmetic, minimum slack 0 at host 0 (the empty graph), binding host 3K₂ at slack 1.8·10−14, ε needed 1.991·10−11; the Lean's 38 literal moment tables equal 720 × that seat's independently computed symmetrised Gram matrices on all 42,142 entries (2,894 nonzero), 0 mismatches; weighted probes on 356 small graphs and 12 named graphs (Grötzsch the closest non-Clebsch graph, margin 2.2·10−3) find nothing below −γ, and no reweighting of the Clebsch graph does either. (iii) The kernel replay of the Lean, below. (iv) A sources seat that fetched every cited statement and the live
tracker, and found the state of BCL described above. (v) The elementary-input control: efps_variant.py shows that with the elementary
n²/18 max-cut bound in BCL's place the argument gives ≥ 0.0299, so no part of the gain over 27/1024 survives without BCL 2(a) or 2(c). Reader-facing numbers in this
entry come from those scripts, not from the paper.
What the Lean proves, and what it does not. The endpoint Erdos128.ModuloBCL.sparse_half_131_5000 has the type
"BCLEventual → for every finite V and triangle-free G on V, ∃ S with |S| = ⌊|V|/2⌋
(natural-number division) and |E(G) ∩ S(2)| ≤ (131/5000)·|V|²", where BCLEventual is
"∃ N, every triangle-free graph on ≥ N vertices has a bipartition with ≤ (2/47)n² internal edges" — Theorem 2(a) of BCL, neither
weakened nor strengthened (our Lean seat unfolded every definition: edgeCountOn is the edge set intersected with the unordered pairs of
S, the diagonal being harmless; the hypothesis quantifies over Type, as the upstream Formal Conjectures statement does). A second
endpoint restates the bound in the exact shape of FormalConjectures/ErdosProblems/128.lean with (1, 50) replaced by (131, 5000); the (1, 50)
instance differs from the upstream body only by 1 * n^2 versus n^2, which our probe closes with one_mul (that rfl fails is the Lean seat's reading of Nat.mul, not kernel-tested) — the Lean docstring's
word "definitionally" overstates that by one lemma. Across the 683 files there is no sorry, admit, axiom,
native_decide, implemented_by, extern, unsafe, partial or opaque declaration
(the one "opaque" is a word in a docstring); maxHeartbeats 0 appears in 506 files, all generated host-check, host-checkpoint and orbit-classification data, and lifts an elaborator limit, not
a kernel one. The C₄ inequality is not an input: the kernel checks a 6-vertex orbit classification (14 parents × 32 profiles) plus 38 host evaluations,
and GlobalBridge.lean sums the mask inequality over all n⁶ maps Fin 6 → V — sampling with replacement, repeated vertices
becoming non-adjacent twins — so the statement proved is C4FlagCertificate G for every finite triangle-free G, with no side condition on
n. The 34 rational terms in C4Certificate/Data.lean are the 34 terms of the JSON certificate, weight for weight and vector for vector
(exact rationals; the Lean proof does not read the JSON). The BCL bridge takes k = N + 1 copies, proves the blow-up triangle-free and the
normalised internal-cut cost invariant. What the Lean does not do: prove BCL, or anything about 1/50.
Our kernel replay (12–13 October). lake build of the whole package on this box against Mathlib v4.30.0 at commit c5ea0035 — the claim's own pin — completed (9,157 jobs; the first attempt was killed at one host checkpoint by the box's memory guard and resumed); #print axioms under the author's audit file prints exactly [propext, Classical.choice, Quot.sound] for all five audited declarations (the two endpoints, the two providers and the certificate theorem); our probe prints the endpoint's full type (pp.all) and every definition it uses — read together they say the sentence in quotation marks above — and a probe theorem proves the Formal-Conjectures-shaped endpoint equal to the upstream body with (131, 5000) by Iff.rfl and the (1, 50) instance by simp only [Nat.one_mul]; a sorry negative control shows sorryAx where it should, and a deliberately wrong-shaped restatement fails to typecheck. statement_match.txt: MATCH, meaning five audit lines and seven probe lines on the standard axioms, sorryAx in the negative control, wrong-shape exit ≠ 0. A leanchecker --fresh pass over the whole import closure (which re-checks the cached Mathlib object files too, not just the proof) ran once the other replay's build had landed: started 13 October 09:50Z at nice 19 on eight cores, it exited 0 after 12,796 s (3 h 33 min) and printed nothing — which is what a pass looks like from this tool; the same binary pointed at a module that does not exist exits 1 in 15 s with Could not find any oleans, so its silence is a verdict, not blindness. (The driver's first launch had been stopped after 60 s to leave memory for the other replay — the 143 row in steps.tsv.) Label (d) for the Lean; the mathematics it checks is labelled above.
Two errors on the live problem page (Bloom's text, not Sarid's; staged for Patrick to send, nothing sent). The page says "Krivelevich [Kr95] has proved this with n/2 replaced by 3n/5 (and 50 replaced by 25)". That statement is false: Kn/2,n/2 is triangle-free, yet every set of 3n/5 of its vertices spans at least n²/20 > n²/25 edges (put x vertices on one side: x(3n/5 − x) is least at x = n/2). Krivelevich's Theorem 4′ gives β = (2α − 1)/4 at α = 3/5, i.e. n²/20, which is what the page should say. And "Erdős, Faudree, Rousseau, and Schelp [EFRS94] proved that this is true with 50 replaced by 16" understates them: 1/16 is the random half (and the page's own α³/2 at α = 1/2); EFRS proved 1/30, as Krivelevich (1995) reports ("the authors obtained the bound β ≤ 1/30") and Razborov (2022) repeats ("[EFRS94] proved that β(G) ≤ 1/30"). We could not reach the EFRS primary (ScienceDirect 403s a datacenter address), so the 1/30 is quoted through those two.
What is ours, and where to look. Nothing in the bound is ours; the referee report is. Three things in it a combinatorialist might want: (i) the dependence on BCL is quantified — the constant n²/18 in its place gives 0.0299–0.0301, and the best public density-dependent inputs still only reach 0.0265, so none of the gain survives without the max-cut input, and 27/1024 remains the unconditional record; (ii) the C₄ inequality is tight at the Clebsch graph and the whole high-density branch is carried by a flag certificate that needs 1.991·10−11 of its 2·10−11 allowance (99.55%; binding host 3K₂ at slack 1.8·10−14; a 1% change to any weight breaks it) — a reader who wants to break the argument should look there, or at the "n large enough" in BCL (which the blow-up lemma removes, correctly, so that is not a hole); (iii) the two live-page errors. What we could not check: BCL 2(a) itself (we found no public certificate, so we could not), the EFRS 1994 and Erdős 1997 primaries (paywalled from a datacenter), and whether the GitHub author is the arXiv author of the same name. Labels: (b) for the theorem, (d) for the certificate and the Lean, (a) for every other lemma. Status LIVE — the claim stands on the tab, refereed, conditional — not ours, problem OPEN. Nothing has been sent to the author, to Bloom or to the tracker.