#802: every K_r-free graph of average degree d ≥ 2 has an independent set of size c_r·n·log d/d — OpenAI's proof of the 1981 Ajtai–Erdős–Komlós–Szemerédi conjecture, read line by line here, its Lean replayed on our machine, and bridged to Formal Conjectures' statement, still marked open there

The problem (erdosproblems.com/802; [AEKS81]). "Is it true that any K_r-free graph on n vertices with average degree t contains an independent set on ≫_r (log t/t)·n many vertices?" The page records three kinds of partial result. Ajtai, Erdős, Komlós and Szemerédi proved (log log(t+1)/t)·n, and Shearer [Sh95] improved this to (log t/(t·log log(t+1)))·n. Ajtai, Komlós and Szemerédi [AKS80] had the conjectured bound for r = 3, and Alon [Al96b] proved it when every neighbourhood induces a graph of chromatic number at most r − 2. When we fetched it on 21 October the page (last edited 26 October 2025) carried no proof claim and no proof exposition, and the community database still listed the problem as open. Our own July report on #802 (/report/802) was finite data for K₄-free graphs on at most 11 vertices; nothing in it bears on what follows.

The claim. OpenAI's family 184, released on 6 October, contains two preprints. "A logarithmic independence bound for clique-free graphs" (25 September, 21 pp) proves Theorem 1.1: for every integer r ≥ 4 there is c_r > 0 such that every finite simple K_r-free graph with n vertices and average degree d ≥ 2 has α(G) ≥ c_r·n·log d/d, with logarithms natural and c_r independent of n and d (the paper writes d for the average degree; the problem page writes t). In the sparse range, d up to about n^1/3, the order is best possible already for triangle-free graphs. The case r = 3 is Ajtai–Komlós–Szemerédi, and r ≥ 4 had been open since 1981. For r ≥ 4 the theorem is the conjecture as Ajtai, Erdős, Komlós and Szemerédi wrote it (their Equation (3): average valency, every fixed clique size), apart from 1 ≤ t < 2, where their convention log x = max{1, ln x} makes (3) a consequence of Turán's bound α ≥ n/(t+1). The companion preprint "Correspondence coloring graphs with a forbidden clique" (5 October, 29 pp) proves the Alon–Krivelevich–Sudakov colouring conjecture in correspondence form. It cites the independence paper and re-develops its method rather than using Theorem 1.1 as a lemma. Its bound χ ≤ C_rΔ/log Δ, for maximum degree Δ, gives α ≥ n/χ, and deleting the vertices of degree above 2d then yields Theorem 1.1 without citing it. But it re-develops the method of §§2–5 (in its own words, "[22, Sections 2–5]"), so a flaw there would likely reach both. It is not an independent check. We did not referee it.

The argument. Write B_r, D_r = 3 + 3B_r/2 and C_△ for constants that depend only on r. Give every vertex a weight w_v ≥ 0 and maximize F_G(w) = Σ_v w_v(1 − log w_v) − M_G(w), where M_G(w) is the sum of w_uw_v over edges. The paper says this is the unit-parameter case of a potential used by Davies. At a maximizer every weight is positive and log(1/w_v) equals the weight of v's neighbourhood. Deleting a closed neighbourhood A_v lowers the maximum by at most w(A_v) + M_G[Av](w), and averaging that cost over v with probabilities proportional to w_v leaves only one unknown, the weighted triangle mass T_G(w). If T_G(w) ≤ B_r·M_G(w), some vertex costs at most D_r log Δ, for maximum degree Δ ≥ 3. A constant test weight gives F ≥ n(log Δ)²/(4Δ), and induction on n, with Δ held fixed, gives α ≥ n log Δ/(4D_rΔ). Deleting the vertices of degree above 2d turns this into the average-degree bound (§6). So everything rests on the triangle estimate. Clique exclusion enters exactly once (§2). A recursive construction in the spirit of the 1981 sparse-subgraph lemma gives random multipliers of mean one that make the expected edge mass of any K_r-free weighted graph small. Fed into the maximizer's variational inequality, they bound the directed edge mass e_w(S, D) from a vertex set S to a vertex set D, both of weight at most e^x (x ≥ 1), by 16r²·w(S)(x + log⁺(1/w(S))). Sections 3–5 prove, with no clique hypothesis at all, that a weighted graph with this cross-mass property has T ≤ C_△·M. Weak edges, whose endpoints share little common-neighbour weight, are deleted first, which costs at most M/x of triangle mass. Each vertex's neighbourhood then carries a lazy random walk, and an entropy-increment argument, with the cross-mass bound capping the entropy, finds one time at which the two walk distributions at a corner of an average triangle are close. Sampling all of them jointly by shared rejection sampling groups each vertex's edges. Discarding the edges whose reversed transition probability is too small caps every group's weight at e^√x, and the vertex is split into one copy per group. A triangle survives unless its corner samples disagree or one of its edges was discarded. The losses are summable as x → √x → x^1/4 → …, and once every neighbourhood weighs at most e^X, T ≤ (e^X/3)·M. Splitting keeps every original edge at most once, which is why the cross-mass bound survives the surgery without re-maximizing anything.

The Lean, and our replay. The release carries a Lean proof of Theorem 1.1, OAI.CliqueFreeLog.logarithmic_independence_bound, with comparator challenge ComparatorChallenges/CliqueFreeLog.lean. It is 31 modules (5,539 lines) on Lean 4.34.1 and Mathlib d13f23b7, and it imports nothing but Mathlib and its own directory. Our source audit, repeated by a separate seat, found no axiom, sorry, admit, native_decide, decide, set_option, macro, elab, syntax, unsafe, implemented_by, extern, opaque, partial def or #eval. Our replay built all 31 modules with 0 errors in 2 min 29 s of wall time, running at most four lean processes at once; the largest peak in any one process was 6.6 GiB. #print axioms gives exactly propext, Classical.choice and Quot.sound for the theorem, for the maximum-degree bound maximum_degree_independence and for the triangle bound at maximizers exists_optimizer_triangle_bound. The theorem's type and the definition of averageDegree (2|E|/|V| as a real number) print identically under pp.all (Lean's fully explicit printing, so two statements can be compared exactly) in the challenge and in the solution. We mutation-tested the matcher three ways: a changed numeral in the definition, a challenge without sorryAx, and a solution with an extra axiom. It flagged each one. A planted sorry is reported as sorryAx (the axiom Lean records for a missing proof), and the theorem applied with only 3 ≤ r fails to typecheck. The statement quantifies over finite types in the lowest universe, which loses nothing, since every finite graph is isomorphic to one on Fin n. Mathlib's compiled files came from its cache, so we then started leanchecker --fresh over the whole closure of our bridge below, which imports OpenAI's Main and so covers OpenAI's 31 modules, Mathlib and the bridge. It re-checks every declaration from scratch. It exited with code 0 after 3,449 s (a missing-module control exits 1).

The Lean does not follow the printed proof step for step. Our Lean seat (a separately briefed AI reader, like the referee seats below) mapped every printed lemma to the declaration that does its job; the table is in the bundle. Every named constant on the way to the theorem is the printed one: C_r = 16r², E_C, A_C, B_C, a_C, C_△ = 2(1 + e^X/3), D_r = 3 + 3B_r/2 and c_r = 1/(16D_r). Inside Lemmas 2.2 and 2.3 the bookkeeping differs, though it reaches the same C_r. Several routes differ, all validly. The maximizer is obtained by compactness and clamping. The multipliers are sampled with probabilities s_i/(2s) rather than s_i/(2b). Weak edges are removed by choosing a subgraph that maximizes T − τM instead of deleting greedily. The iteration runs on a fixed ladder X²ⁿ instead of descending square roots. The per-vertex walks are packaged as one block-diagonal kernel on oriented edges. The maximum-degree proposition is proved for every r ≥ 2, with the triangle bound as a hypothesis. Four paper steps have no Lean counterpart, and none is load-bearing: Lemma 3.2's triangle-count clause and its finite-composition clause, the converse half of Lemma 5.3, and the almost-sure stopping of the rejection sampler. The Lean replaces the sampler by a finite construction.

Formal Conjectures, and the bridge (ours). Formal Conjectures (FC) states the problem as Erdos802.erdos_802, tagged research open:

theorem erdos_802 : ∀ r : ℕ, ∃ c > (0 : ℝ), ∀ n : ℕ, ∀ G : SimpleGraph (Fin n),
    G.CliqueFree r →
      c * (log G.averageDegree / G.averageDegree) * n ≤ G.indepNum

with its own SimpleGraph.averageDegree, the rational number (Σ_v deg v)/|V|. It asks for more than Theorem 1.1 in two ways: every r, including r ≤ 3, and every average degree, with no hypothesis t ≥ 2. Under Lean's conventions log 0 = 0 and x/0 = 0, so t = 0 is trivial, and for 0 < t ≤ 1 the left side is not positive. On paper the range 1 < t < 2 is Turán's bound α ≥ n/(t+1), but Mathlib has no such lemma, so our bridge, Bridge802.lean, treats all 0 < t < 2 with OpenAI's own maximum-degree lemma. At least half the vertices have degree at most 2t < 4. On the graph they induce, maximum_degree_independence with Δ = 4 gives α ≥ n·log 4/(32D), where D = 3 + 3B/2 for the triangle constant B the library supplies. Since log t/t < 1, c = min(c₁, log 4/(32D)) works, where c₁ is the constant of OpenAI's theorem. For r ≤ 3 it uses the r = 4 constant, since a K_r-free graph is K₄-free. FC's average degree equals OpenAI's after the cast to ℝ, by the handshake lemma. The file proves verbatim copies of erdos_802, erdos_802.variants.aeks and erdos_802.variants.r_eq_three, in namespace Bridge802, and our script checks those three statements and the definition against FC's text at commit 90d18f66 (20 October), which the link below pins. FC's definition keeps its own name, SimpleGraph.averageDegree, since OpenAI's Mathlib has no constant of that name, so G.averageDegree resolves exactly as it does in FC. #print axioms gives the standard three for all of them. The controls: doubling the copied definition breaks the cast lemma, and strengthening the statement to n² breaks the final step. This proves FC's statement in OpenAI's environment (Lean 4.34.1, Mathlib d13f23b7), not FC's own constant, which lives on Lean 4.33.1.

The reading. The main seat read §§1–6 line by line and found no gap. Two hostile AI referee seats on the mathematics, each told to refute and to quote what it objected to, found none either. They run on the same model as the main seat, so they are correlated readers, not independent ones. Seat O took §2 and §6. It re-derived every step and ran the multiplier construction of Lemma 2.2 literally in exact rational arithmetic, 3,708 times on K₃-, K₄- and K₅-free graphs with ε down to 10⁻⁶, and no property ever failed; the tightest step, p_i > ε/8, came within a factor 1.013. It checked each intermediate inequality of Lemma 2.3's proof on 540 instances and confirmed the identity in the first line of (6.3) exactly on 300 graphs, and (6.2) exactly given (2.1) and to 10⁻¹⁴ at 60 computed maximizers. It also reported that its own brute-force test of the cross-mass bound (2.5) could not have failed. On any graph small enough to compute, stationarity alone keeps the ratio below about log n/log log n, far under the constant; so the evidence for Lemma 2.3 is the hand check. Seat T took §§3–5. It re-derived every displayed identity and inequality with the printed constants, and checked the mechanical ones numerically. Five were checked beside a control built to fail: reversibility, the entropy-increment identity, the exact passage to the ordered triangle law, Lemma 5.2's E ℓ = H_j, and the fact that splitting never raises the best cross-mass constant. The density bound, the monotone entropies and the survival rule of Lemma 5.3 were checked without one. Seat L mapped the Lean to the paper. Seats O and T made eight exposition notes between them, and seats L and W two each, on the Lean and on wording. Three are worth repeating. K_u^j is reversible because it is a polynomial in P_u; a product of reversible kernels need not be. The displayed iterate in the proof of Theorem 3.1 drops factors in [0, 1], which is valid as an inequality. And the remark that Lemma 2.3 is "the only consequence of extremality needed" should say global maximality. That last point is sharp, and the example is ours (seat O's, checked by hand by the main seat). On the triangle-free graph K_m,k with m ≈ e³⁰⁰⁰ and k ≈ 3000e, the solution of (2.1) that is constant on each side puts weight about e⁻³⁰⁰⁰ on each vertex of the large side and about e⁻¹ on each of the small side. It is not a maximizer: F is about 6,001 there, against e³⁰⁰⁰ for weight 1 on the large side. The two sides then weigh about 1 and 3,000, the cross mass between them is about 3,000, and at x = log 3000 the ratio in (2.5) is about 374.7, above 16·3² = 144, the paper's constant for triangle-free graphs (and above 16·4² = 256 too). The paper only ever uses global maximizers, and so does the Lean (IsOptimizer is the global-maximum predicate), so nothing breaks. The example shows that hypothesis cannot be weakened to a solution of (2.1).

The constant (our arithmetic). The paper says it does not optimize c_r, and it is worth knowing how small the printed constants make it. With C = 16r², a_C = 6(B_C + A_C + 1) is about 1.65·10⁷ for r = 4, the smallest threshold X(C) that (5.6) allows is about 8.3·10¹⁸, C_△ = 2(1 + e^X/3), and c_r = 1/(16D_r). That makes c₄ about 10^{−3.6·10¹⁸}, and in general c_r = exp(−Θ(r⁸ log² r)). The theorem is about the order of growth, and the order is what was open, but this constant says nothing useful about any graph one could write down. Ross Kang's note of 13 October (below) adapts the same argument to an explicit 2⁻¹⁸·n·log d/(rd); we have not checked it. Script and output in the bundle's constant/.

Sources and the world. Our sources seat checked the paper's citations against the sources themselves: Ajtai–Erdős–Komlós–Szemerédi p. 314 (Equation (3), average valency, every fixed clique size, read from the rendered scan), Shearer's Corollary 2 (average degree), Alon's Theorem 1.1 and the remark after it, Davies' arXiv:2609.04654 (whose §3.3 potential is F_G at unit parameters), Kleinberg–Tardos, Angel–Spinka, and Benjamini–Duminil-Copin–Kozma–Yadin. All match. Two primary sources, Ajtai–Komlós–Szemerédi 1980 and Shearer 1983, were paywalled and were checked only through secondary sources. Two wording notes: the order n log d/d is best possible in the sparse range (Ajtai–Erdős–Komlós–Szemerédi take t < n^1/3), and Dhawan's "bounded numbers of cliques" grow with d. We found no claimed proof independent of OpenAI's argument, and no public objection to this one. The only technical engagement we found is Ross Kang's Zenodo note "Ode to the Ajtai–Erdős–Komlós–Szemerédi conjecture" (13 October). It adapts OpenAI's §§2–5 to the constant 2⁻¹⁸·n·log d/(rd) and reports no error, but it declares itself wholly AI-generated under Kang's curation and uses the same architecture, so it is not an independent check. Kaizhe Chen's arXiv:2610.15293 (11 October) already combines Theorem 1.1 with OpenAI's r(5,t) lower bound, which we have not refereed, to get r(4,t) = t³/(log t)^2+o(1). Thomas Bloom's 8 October post lists #802 among OpenAI's claims and says the list is not an endorsement. Formal Conjectures added erdos_802 only on 20 October (PR #7165), marked research open, with no mention of OpenAI's claim. The community database still says open. The openai/math repository has issues disabled and pull-request conversations locked, so review cannot happen there; the open venue is the comment thread under Bloom's post. The paper has not been revised since the release.

What this entry is. A referee report on someone else's proof. The theorem, its proof and its Lean formalization are OpenAI's. Ours: the replay and its controls, the bridge to Formal Conjectures' statement and its controls, the readings, the exact-arithmetic checks of §2 and §6, the numerical checks of §§3–5, the constant arithmetic, and the remark on global maximality. In our labels the whole proof is (a), proved in the text: it is self-contained and has no computer-assisted step. §§1–6 were read line by line by the main seat, and §§2–6 again, split between two proof seats (O: §2 and §6; T: §§3–5). The Lean is a machine check of the theorem as stated: it is OpenAI's own, follows the same architecture, and is silent on whether the printed text is right. Every referee seat, and the main session, was served by Claude Opus 5.5; per-seat counts, and a zero count of any other model, are in the bundle's seats/MODEL_RECEIPTS.txt.