Counterexamples to Sidorenko’s conjecture and the forcing conjecture

1 paperLean

Disproves Sidorenko's conjecture with a connected bipartite pattern on 35 vertices and 66 edges that occurs less frequently than in a random graph of the same edge density. The same pattern disproves the forcing conjecture of Skokan and Thoma: matching its density and the edge density of a constant graphon need not force quasirandomness.

Watch

▶Introduction: the problem and why it mattersin preparation

▶The presented solutionin preparation

Papers 1

A counterexample to Sidorenko's conjecture

OpenAI · September 23, 2026

We disprove Sidorenko's conjecture with a bipartite graph on 35 vertices and 66 edges: its homomorphism density in some finite simple graph is smaller than the conjectured lower bound. The same connected graph also disproves the forcing conjecture: at one fixed density, asymptotically matching the edge and pattern densities does not imply quasirandomness.

Read PDF Download Source

Cite

@misc{OAI:A-counterexample-to-Sidorenkos-conjecture-September-23-2026,
  author = {{OpenAI}},
  title = {{A counterexample to Sidorenko's conjecture}},
  howpublished = {OpenAI Math Release preprint
                  \href{https://github.com/openai/math/blob/main/preprints/A-counterexample-to-Sidorenkos-conjecture-September-23-2026/paper.pdf}{OAI:A-counterexample-to-Sidorenkos-conjecture-September-23-2026}},
  year = {2026}
}

What was formalized in Lean

The following describes the scope of the Lean formalization related to the following accompanying paper(s):

A counterexample to Sidorenko's conjecture

Scope

Sidorenko's conjecture predicts that every bipartite graph \(H\) has homomorphism density at least the host graph's edge density raised to \(|E(H)|\). The formalization disproves this for the paper's fixed bipartite graph with \(35\) vertices and \(66\) edges: it constructs a nonempty finite simple host graph with \(t(H,G)<t(K_2,G)^{66}\). The separate forcing-conjecture consequence in the paper is outside this statement.

Comparator links

Result	Comparator statement
Counterexample to Sidorenko's conjecture	SidorenkoCounterexample.lean

Scope note on GitHub →