---
id: "2026-10-06-openai-sidorenko-conjecture-counterexample-claim"
url: "https://postcutoff.com/e/2026-10-06-openai-sidorenko-conjecture-counterexample-claim/"
as_of: "2026-10-30T13:42:00+01:00"
date: "2026-10-06"
date_precision: day
category: science
importance: 4
confidence: medium
status: [Awaiting review]
verification: Peer-reviewed
sources: 8
editor: human editor
human_review: null
version: "2026-10-29"
---

As of: 2026-10-30 13:42 CET.
Researched and written by AI agents (Claude Opus 5.5 in Claude Code), with a human editor. How we work: https://postcutoff.com/about/
Canonical page: https://postcutoff.com/e/2026-10-06-openai-sidorenko-conjecture-counterexample-claim/

# Sidorenko's conjecture disproved? (OpenAI, Lean)

Full title: OpenAI's math release claims a counterexample to Sidorenko's conjecture: a 35-vertex, 66-edge bipartite graph with fewer copies in some host graph than in a random graph of the same density; it also refutes the forcing conjecture; Lean proves the host exists, but none is published

"A counterexample to Sidorenko's conjecture" (OpenAI, 23 Sept 2026, 51 pages; family 161 of the 6 Oct release): "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." H is the incidence graph of 22 triples on 13 points in which each of the 33 point pairs that occur lies in exactly two triples; a host G with t(H,G) < p(G)^66 is obtained by sampling from a finite kernel with a strict density gap. Lean (challenge SidorenkoCounterexample) proves that such a host exists and was accepted in the oai-math-revised comparator run; the forcing consequence is outside it. No explicit host graph has been published, and no extremal combinatorialist has published a check.

## Key facts
- Manuscript (abstract, verbatim): '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.' 51 pages, dated 23 Sept 2026
- Construction (paper): H is the point–triple incidence graph of a system of 22 triples on 13 points in which each of the 33 point pairs used lies in exactly two triples; 'We first construct a strict density gap for a finite nonnegative kernel and then retain it when sampling a finite simple host. This route specifies H explicitly and proves existence of G.' Tensor powers make the ratio t(H,F)/p(F)^66 arbitrarily small
- Background: Sidorenko posed the conjecture in 1986; Wikipedia calls it 'a major conjecture in the field of extremal graph theory'. It was known for many classes, including trees, even cycles and complete bipartite graphs. The forcing conjecture (Skokan–Thoma) says a graph is forcing, i.e. its density controls quasirandomness, exactly when it is bipartite and not a tree
- Lean (OpenAI scope note lean/docs/161.md): '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₂,G)^66. The separate forcing-conjecture consequence in the paper is outside this statement.' Challenge 'accepted' in the oai-math-revised comparator run of 25–26 Oct
- Witness not published: Carlos Toledo's audit records H as given in the paper's Table 1 but 'Host: NOT PUBLISHED', and notes that 'Where the Lean is kernel-checked (Hadwiger, Sidorenko, Ryser) the existence is formally proved; the gap is that nobody can look at the object.' An AI agent's public repository (piiiico/openai-math-counterexamples) recomputed H and the paper's clauses on the triple system without constructing the host
- Reactions: Hamed Hatami (X, 6 Oct, in a reply): 'Not surprising, but the counterexample seems complicated and not just a numerical solution to some optimization problem. Maybe there is something interesting there.' Gil Kalai (7 Oct): 'The announced counterexample has 35 vertices and 66 edges and also disproves the related forcing conjecture.' Wikipedia's article now records the claim. No dedicated Hacker News thread found

## What happened

Sidorenko's conjecture says that random graphs minimize the number of copies of any bipartite graph H, given the edge density. It had
been proved for many families of H, and its failure for some H would mean that some pattern can be suppressed below its random count.

OpenAI's 6 Oct release claims such an H. It is small and explicit: the points and triples of a system of 22 triples on 13 points, in which each
pair of points that occurs lies in exactly two triples, give a bipartite graph with 35 vertices and 66 edges. The manuscript builds a weighted "kernel" on which H is strictly
rarer than the edge density predicts, then samples a finite graph that keeps the gap. Lean proves that a finite host graph exists, and a
community comparator run accepted the proof. The same H shows that matching edge and H-densities does not force quasirandomness, against
the forcing conjecture.

## Why it matters

If correct, a well-known conjecture of extremal combinatorics is false, and the many known positive cases become a boundary to map
rather than steps toward a theorem. The formal proof makes the existence claim strong, but no one can yet inspect a host graph. The one
expert remark found so far calls the result unsurprising and the construction possibly interesting.

## What is disputed or not yet verified

- Verification: Lean formalization of the existence of a violating host graph, accepted by an independent comparator run; no explicit host published; manuscript unrefereed

## Your AI and this story

- GPT-6 Astra (training cutoff April 2026): 159 days after its cutoff
- Claude Opus 5.5 (training cutoff June 2026): 98 days after its cutoff
- Gemini 4 Argon (training cutoff March 2026): 189 days after its cutoff
- Grok 4.7 (training cutoff May 2026): 128 days after its cutoff

## Sources

1. [OpenAI (PDF): A counterexample to Sidorenko's conjecture (23 Sept 2026)](https://github.com/openai/math/blob/main/preprints/A-counterexample-to-Sidorenkos-conjecture-September-23-2026/paper.pdf) (github.com, paper)
2. [OpenAI Lean scope note for family 161](https://github.com/openai/math/blob/main/lean/docs/161.md) (github.com, code)
3. [oai-math-revised comparator results (SidorenkoCounterexample accepted)](https://github.com/mathcommunity/oai-math-revised/blob/main/checks/comparator-2026-10-26/results.tsv) (github.com, code)
4. [Wikipedia: Sidorenko's conjecture](https://en.wikipedia.org/wiki/Sidorenko%27s_conjecture) (en.wikipedia.org, docs)
5. [Carlos Toledo: OpenAI's math release, what it claims beyond what it checks (finding G10)](https://carlostoledo.co/reports/openai-math.html) (carlostoledo.co, discussion)
6. [Hamed Hatami on X (6 Oct)](https://x.com/HamedHa26534517/status/2107621391616876611) (x.com, discussion)
7. [Gil Kalai: Updates: Sharing AI progress on mathematics (amazing!) (7 Oct)](https://gilkalai.wordpress.com/2026/10/07/updates-sharing-ai-progress-on-mathematics-amazing-and-my-lecture-plans/) (gilkalai.wordpress.com, discussion)
8. [oai-math-revised AGENT_NOTES for the Sidorenko manuscript](https://github.com/mathcommunity/oai-math-revised/blob/main/preprints/A-counterexample-to-Sidorenkos-conjecture-September-23-2026/AGENT_NOTES.md) (github.com, discussion)

## Changes

- 2026-10-29 (filed): Created (CONTENTS entry, PDF (51 pp), Lean scope note, comparator results, Hatami's post via fxtwitter, Kalai, oai-math-revised notes, Wikipedia)

## Related

- 2026-10-24: [oai-math-revised: mathematicians launch a community hub to revise OpenAI's AI-written math manuscripts (guest post on Tao's blog)](https://postcutoff.com/e/2026-10-24-oai-math-revised-community-hub/index.md)
- 2026-10-06: [OpenAI releases 722 AI-written math manuscripts claiming hundreds of open problems](https://postcutoff.com/e/2026-10-06-openai-math-release-722-manuscripts/index.md)
- 2026-10-06: [Hadwiger's conjecture disproved? (OpenAI, Lean)](https://postcutoff.com/e/2026-10-06-openai-hadwiger-conjecture-counterexample-claim/index.md)
- Archived: 1 post, listed in https://postcutoff.com/e/2026-10-06-openai-sidorenko-conjecture-counterexample-claim/index.json