Forbid a clique, gain a log?

0:00The question

Pick some vertices of a graph, no two of them joined by an edge. That is an independent set. If each vertex has on average d neighbors, there is always one with at least n/(d+1) of the n vertices, and disjoint cliques show that you cannot do better: 3 separate groups of 4, each fully joined, allow only one vertex per group. Forbid triangles, and the answer grows. In 1980, Ajtai, Komlós and Szemerédi proved that triangle-free graphs have independent sets of order n log d/d, a gain of a factor log d. Coloring is the same question in reverse: color the vertices so that neighbors differ, and each color is an independent set. If no vertex has more than Δ neighbors, Δ+1 colors always suffice, and for triangle-free graphs, Johansson brought that down to order Δ/log Δ, even for list coloring. What if we forbid a larger clique, say 4 vertices all joined to each other? In 1981, Ajtai, Erdős, Komlós and Szemerédi conjectured the same log d gain for every fixed forbidden clique, and proved a gain of log log d. In 1995, Shearer reached n log d/(d log log d), and later work, as the papers recount, kept a log log loss. Coloring followed the same pattern: for graphs with no clique of r vertices, Johansson’s bound, and Bernshteyn’s version for a stronger kind of coloring, kept a factor log log Δ. In 1999, Alon, Krivelevich and Sudakov conjectured that forbidding any fixed graph allows order Δ/log Δ colors.

1:41The claim

Result 184 is two OpenAI preprints. The first, 21 pages, dated September 25, 2026, claims the independence conjecture: for every r at least 4, there is a positive constant c_r such that every graph with no r-clique and average degree d at least 2 has an independent set of at least c_r times n log d/d. The second, 29 pages, dated October 5, claims the coloring version: for every r at least 4, there are constants such that every graph with no r-clique and large enough maximum degree Δ can be correspondence colored from lists of a constant times Δ/log Δ entries. Every fixed graph sits inside a large enough clique, so the same holds when any fixed graph is forbidden. The paper says this proves the Alon, Krivelevich and Sudakov conjecture in a stronger form. Correspondence coloring, also called DP coloring after Dvořák and Postle, is that stronger form. Each vertex has its own list of entries, and each edge carries its own rule that pairs up entries at its two ends, and paired entries clash. The rules need not agree around a cycle. A square shows the difference. Two colors suffice, and in our check, so does every assignment of two-color lists. But give each corner two entries, with the rules straight along three sides and crossed along the fourth, and every choice runs into a clash. With such rules, the square needs 3 entries per corner. So a bound for correspondence coloring covers list coloring and ordinary coloring too. Not claimed: usable constants. The independence paper’s constants are explicit, but with its own choices, our arithmetic puts the constant for 4-cliques below 10 to the minus 3.6 billion billion. The coloring paper’s constants are only shown to exist; its own choices make the color constant at least 1.6 million, so the bound beats the easy Δ+1 only when Δ has at least about 700,000 digits. Neither paper claims an algorithm. The order n log d/d is best possible, as the independence paper notes, but no coefficient is claimed: the Paley graph on 17 vertices, pictured earlier, has no 4-clique and no 4 independent vertices, though n log d/d is about 4.4.

4:08How the proof goes

The independence proof weighs the vertices. Give each vertex a nonnegative weight, and score the weights: the sum of w times one minus log w, minus the total weight of the edges, each edge weighing the product of its ends. Weight one on an independent set scores its size, so the best score is at least the independence number, and the proof shows that the independence number is at least the best score divided by a constant times log Δ. At the best weights, each vertex weighs e to the minus the weight of its neighbors. Now peel: keep one vertex, delete it with its neighbors, and repeat. Each deletion lowers the best score by at most the deleted weight plus the weight of the edges among the deleted vertices, and each edge among a vertex’s neighbors makes a triangle with it. In our small example, this keeps 5 vertices, the most possible. So everything hinges on one bound: at the best weights, triangles must cost at most a constant times the edges. First, testing the best weights against random perturbations bounds the edge weight between any two sets, using the recursion of Ajtai, Erdős, Komlós and Szemerédi: when no r vertices are all joined, no r − 1 neighbors of a vertex are all joined. Second, a separate theorem, with no clique hypothesis at all, turns that into the triangle bound by splitting vertices. If every neighborhood were light, triangles would be few. So split a vertex into copies of the same weight, and hand each copy some of its edges, each edge used once; the bound between sets survives the split, but a triangle whose edges go to different copies is lost. To decide which edges travel together, run a lazy random walk inside each neighborhood. An entropy count shows that at some step, walks started at two corners of a typical triangle look alike, and a shared sampling scheme then usually gives them the same label, so most triangles survive. Each round shrinks the neighborhood weights from e to the x to e to the square root of x, and the triangles lost over all rounds add up to less than the whole, so a fixed share survives until the neighborhoods are light. The paper credits the score to Davies, and the entropy and sampling tools to earlier work that it cites. The coloring paper reuses this engine in a Johansson-style process: color in many small random rounds. Every list entry carries a weight. In each round, entries switch on at random, an entry that switches on becomes its vertex’s color if no clashing entry next door switches on, and the other weights are adjusted to compensate. The enemy is again triangles, now in the graph whose vertices are list entries and whose edges are clashing pairs, which also has no r-clique. A new adjustment lemma, proved by duality from a triangle bound of the same kind, finds local reweightings that offset the triangle cost, up to a constant times the edge cost, everywhere at once. What correspondence coloring adds is that there are no shared color names, so each adjustment must also touch only a limited number of entries of any one list; that gives the concentration the rounds need. The Lovász local lemma lets every vertex progress at once, and at the end, greedy coloring finishes the job.

7:27Where it stands

Both preprints are unrefereed and have not been revised. OpenAI’s Lean files state the independence theorem exactly, and prove it in 31 files and about 5,500 lines, with no gaps we could find by search; we did not run the check. The Lean statement, like the theorem, says that a constant exists, without giving its value. The coloring theorem, the headline of this entry, is not formalized. Neither paper is among those OSVerify reviewed, and we have seen no expert review. If they hold, forbidding any fixed clique buys the same log factor as forbidding triangles, for independent sets and for coloring, even correspondence coloring, though with constants far too weak to matter for any graph anyone could write down.