AI Proved What?

Episode 161, October 2026

Sidorenko disproved?

A preprint claims a bipartite pattern on 35 vertices that some finite graph contains less often than a random graph of the same edge density

Covers result 161 in OpenAI’s catalog: its one paper. See its connections to other results and the work it cites.

Play Episode 161: Sidorenko disproved? Twenty-two yellow triangles with blue vertices forming a polyhedron, our drawing of the pattern as a triangulated sphere.

6:29. English captions available. The video loads from YouTube when you press play.

Chapters

  1. 0:00The conjecture
  2. 1:59The claim
  3. 3:34How the proof goes
  4. 5:34Where it stands

The claim, in plain words

Throw the vertices of a small pattern graph H onto a big host graph G at random, allowing repeats. The homomorphism density t(H,G) is the chance that every edge of H lands on an edge of G. If G is random with edge density p, it is about pe(H). Sidorenko’s conjecture “asserts that t(H,G) ≥ p(G)|E(H)| whenever H is bipartite and has at least one edge”, where p(G) = 2|E(G)|/|V(G)|2: randomness is the worst case. As the paper recounts, it grew out of supersaturation questions, Sidorenko formulated it (1991, 1993), and it was proved for trees, even cycles and complete bipartite graphs, by Conlon, Fox and Sudakov when one vertex is joined to the whole other side, for hypercubes by Hatami through graph norms, and for many further classes (Kim, Lee and Lee; Conlon and Lee; others); Lovász proved it for weighted hosts close enough to constant.

Result 161 is a single OpenAI preprint, A counterexample to Sidorenko’s conjecture (51 pages, dated September 23, 2026). Its pattern is explicit: H is the incidence graph of 22 triples on 13 points listed in Table 1, a connected bipartite graph with 35 vertices and 66 edges in which every pair of points in a triple lies in exactly two triples (as we noticed, the 22 triangles tile a sphere). Theorem 1.1: “There is a finite simple undirected graph G with at least one edge such that t(H,G) < p(G)66.” The same H disproves the forcing conjecture, which Conlon, Fox and Sudakov formulated following a question of Skokan and Thoma: at one density p there is a nonconstant graphon W with t(K2,W) = p and t(H,W) = p66.

What it doesn’t claim

The paper explains why H escapes several known positive criteria, but the host is proved to exist, not written down, and the paper puts no number on its size or on the shortfall; by our rough reading of the proof’s own estimates, the hosts it guarantees are astronomically large and the shortfall a tiny fraction. Tensor powers push the density of H as far below the random value, proportionally, as you like, while the edge density shrinks; blow-ups give fewer genuine copies than random by a fixed fraction at a fixed density. The forcing failure is shown at one density only (“does not assert failure of p-forcing at every density”), and the paper says nothing about smaller counterexamples or other open cases. The catalog attributes the forcing conjecture to Skokan and Thoma; the paper credits its formulation to Conlon, Fox and Sudakov.

Where it stands

Posted as a preprint
OpenAI, 51 pages, dated September 23, 2026
Peer reviewed
Not yet
Checked in Lean
Exactly the main theorem; the forcing corollary is not formalized. We have not rebuilt it

Last checked October 19, 2026. The preprint has not been revised since it was added to the repository in its initial commit on October 6, 2026. OpenAI published a Lean formalization of exactly the main theorem (comparator, with the pattern copied from the paper’s table and homomorphisms counting all maps), in 35 files and 23,761 lines excluding Mathlib (development). Finite facts about H are checked by computation inside Lean, but the inequality is proved, and, like the paper, Lean shows the host exists without building it. We found no unproved steps, and we have not rebuilt it. The corollaries, including the forcing conjecture, are not formalized. The paper is not among those OSVerify reviewed, and we have seen no expert review.

How the proof goes

  1. Two steps. First a weighted host: a kernel on a finite probability space with t(H,U) < μ66, μ its mean. Then sampling: once sampled graphs have enough vertices, at least one has t(H,G) < p(G)66 (Lemma 3.6).
  2. Half-rank tests. Host vertices carry random symmetric matrices over a finite field, and an edge weight asks whether a difference of two matrices has exactly half the full rank, with a prescribed sign: whether the determinant of its nonzero part is a perfect square. Half rank pins the sign attached to two point matrices meeting a shared triangle’s matrix, up to a fixed sign, to the product of the prescribed signs; as the field grows, the 33 pair signs behave like independent fair coins.
  3. Parity and one negative term. Each pair lies in exactly two triangles, so its coin averages away and leaves the parity of the four corner signs around it. A random choice at each corner, with one corner biased the other way, leaves a single negative term −(θ/2)66 at the intended arrangement, which colour-refinement scores make dominant. Dilution and symmetrisation give the kernel; the longest part of the paper bounds rare singular configurations with symplectic geometry, with a large matrix dimension (above 1,641 for one estimate) fixed before the field size goes to infinity.
  4. Forcing. Mixing the bad host with a kernel of too high a density of H gives, at some mixture, exactly the random density of H, while the four-cycle density stays above random, so the mixture is not quasirandom.

The numbers in the video

  • Our rebuild of H from Table 1: 35 vertices, 66 edges, bipartite, connected; point degrees 4 (three), 5 (six), 6 (four); 33 pairs, each in exactly two triples; Euler characteristic 2 with every vertex link a cycle, so a triangulated sphere (ours).
  • Our ratios t(F,G)/p(G)e(F) on 30-vertex hosts (random, K15,15, two K15’s, a star) for P3, C4, K2,3, C6 and H: all at least 1.
  • Our stand-in for the forcing argument, with triangles (not bipartite): the mixture at s = 2/3 has triangle density exactly 1/8 = p3, while the four-cycle density is 0.06404, above p4 = 0.0625.
  • The Lean counts: 35 files and 23,761 lines, our count of the import closure.

Read the source

The paper

OpenAI groups related papers into one result; this one has a single paper.

Transcript

Read the full script

0:00The conjecture

Pick a small pattern graph H and a big host graph G. Throw the vertices of H onto G at random, allowing two of them to land on the same vertex. The chance that every edge of H lands on an edge of G is the homomorphism density of H in G. If G is random with edge density p, that chance is about p to the power of the number of edges of H. Sidorenko’s conjecture says that when H is bipartite, no host with edge density p does worse: randomness is the worst case. For a triangle, which is not bipartite, it fails at once, since a complete bipartite host contains no triangles at all. As the paper recounts, the conjecture grew out of questions about how many copies of a pattern must appear once a graph has many edges, and Sidorenko formulated it in the early 1990s. It was proved for trees, even cycles and complete bipartite graphs; by Conlon, Fox and Sudakov when one vertex is joined to the whole other side; for hypercubes by Hatami, through graph norms; and for many further classes, by Kim, Lee and Lee, Conlon and Lee, and others. Lovász showed it holds for weighted hosts close enough to constant, how close depending on the pattern. In our check of small patterns, and of H itself, on 30-vertex hosts, random and structured, the inequality always held, often with room to spare. A related question is about randomness itself. Chung, Graham and Wilson showed that a sequence of graphs with the random densities of edges and of four-cycles must, in the limit, contain every small pattern as often as a random graph does. The forcing conjecture, formulated by Conlon, Fox and Sudakov following a question of Skokan and Thoma, says that every bipartite graph containing a cycle can replace the four-cycle here. They note that it is stronger than Sidorenko’s conjecture.

1:59The claim

Result 161 is a 51-page OpenAI preprint, dated September 23. Its pattern is explicit: 13 points and 22 triples of them, listed in a table. H joins each point to the triples containing it, giving a connected bipartite graph with 35 vertices and 66 edges, and every pair of points in a triple lies in exactly two triples. As we noticed, the 22 triangles tile a sphere. The theorem: some finite graph G, with at least one edge, has homomorphism density of H below its edge density to the 66th. If the proof holds, Sidorenko’s conjecture is false. The same H disproves the forcing conjecture: at one density, a graphon that is not constant matches the random densities of edges and of H exactly. The paper explains why H escapes several known positive criteria, but it does not write the host down: G is proved to exist, and the paper puts no number on its size or on the shortfall. By our rough reading of the proof’s own estimates, the hosts it guarantees are astronomically large, and the shortfall a tiny fraction. Repeated products push the density of H as far below the random value, proportionally, as you like, though the edge density shrinks as they do. Blowing the host up also gives fewer genuine copies of H than random, by a fixed fraction, at a fixed density. The forcing failure is shown at one density, and nothing is said about smaller counterexamples or other open cases.

3:34How the proof goes

The route has two steps. First build a weighted host, a kernel on a finite probability space, with too low a density of H; then sample finite graphs from it, and once they have enough vertices, at least one keeps the shortfall. The kernel’s raw material is random symmetric matrices over a finite field. Each vertex of the host carries such matrices, and an edge weight asks whether a difference of two matrices has exactly half the full rank, with a prescribed sign: whether the determinant of its nonzero part is a perfect square in the field. Half rank forces a coincidence: when two point matrices both meet the matrix of a shared triangle this way, the sign attached to their difference is pinned, up to a fixed sign, to the product of the two prescribed signs. As the field grows, the 33 pair signs behave like independent fair coins. Each pair lies in exactly two triangles, so its coin appears twice and averages away, leaving only the parity of the four corner signs around that pair. A random choice at each corner, with one corner biased the other way, then leaves a single negative term at the intended arrangement, and scores from colour refinement make it outweigh the rest. Diluting and symmetrising gives a kernel whose density of H is below its edge density to the 66th. The longest part of the paper bounds rare singular configurations, using symplectic geometry; the proof fixes a large matrix dimension, above 1,641 for one estimate, before letting the field size go to infinity. For forcing, the paper mixes the bad host with a kernel that has too high a density of H and finds a mixture with exactly the random count that is still not random. In our stand-in with triangles, which are not bipartite, the mixture hits the random triangle count exactly, while the four-cycle count stays above random.

5:34Where it stands

The paper is not peer reviewed and has not been revised. OpenAI’s Lean formalization states exactly the main theorem, with H copied from the paper’s table, in 35 files and about 24,000 lines. Finite facts about H are checked by computation inside Lean, but the inequality itself is proved, and, like the paper, Lean shows the host exists without building it. We found no unproved steps, and we have not rebuilt it. The corollaries, including the forcing conjecture, are not formalized. The paper is not among those OSVerify reviewed, and we have seen no expert review. If it holds, randomness is not always the worst case for bipartite patterns: this 35-vertex pattern can be undercut, though, by our estimate, any host the proof guarantees is far too large to write down.

Spot a mistake?

This episode simplifies on purpose, but it shouldn’t be wrong. If something is, open an issue on GitHub or leave a comment on YouTube. Corrections are noted here with a date.