Aftermath bot: New page for the counterexample to Sidorenko's conjecture and the forcing conjecture with public follow-ups

2026-10-18T09:46:53Z

New page for the counterexample to Sidorenko's conjecture and the forcing conjecture with public follow-ups

New page

'''Sidorenko's conjecture''' asserts that for every bipartite graph ''H'' with at least one edge and every graph ''G'', the homomorphism density of ''H'' in ''G'' is at least the edge density of ''G'' raised to the number of edges of ''H''. A manuscript dated 23 September 2026 in OpenAI's public mathematics collection ([https://github.com/openai/math github.com/openai/math]) claims a counterexample, a connected bipartite graph with 35 vertices and 66 edges, and with it a counterexample to the forcing conjecture of Conlon, Fox and Sudakov. This page summarizes the published claim and lists publicly available follow-up work. Statements are the respective authors' claims; the publication of a paper, code or a formal proof is not presented here as independent verification.

== Background ==
* As recounted in the introduction of the manuscript:
** The conjecture grew out of supersaturation questions studied by Erdős, Lovász and Spencer and by Simonovits; Sidorenko formulated the inequalities for nonnegative kernels (1991, 1993). The homomorphism count includes noninjective maps.
** Trees, even cycles and complete bipartite graphs are basic positive cases. Conlon, Fox and Sudakov proved the conjecture when one vertex is adjacent to the entire opposite part. Hatami developed the graph-norm approach, and Conlon and Lee constructed weakly norming graphs from reflection groups. Li and Szegedy, Szegedy, Kim, Lee and Lee, and Conlon, Kim, Lee and Lee proved gluing, entropy and tree-decomposition results, and Conlon and Lee and later Coregliano gave degree-count criteria.
** A graph ''F'' is ''forcing'' if, for every edge density, convergence of the edge density and of the ''F''-density to their values in the random graph forces quasirandomness. Chung, Graham and Wilson showed that the four-cycle is forcing, Skokan and Thoma studied which bipartite graphs can replace it, and Conlon, Fox and Sudakov conjectured that a graph is forcing if and only if it is bipartite and contains a cycle. The forcing conjecture is stronger than Sidorenko's conjecture.

== The original result ==
* '''Claim.''' Theorem 1.1 of the manuscript states that the incidence graph ''H'' of an explicit system of 22 triples on 13 points, which has 35 vertices and 66 edges, admits a finite simple graph ''G'' with at least one edge such that ''t''(''H'', ''G'') < ''p''(''G'')<sup>66</sup>, where ''t'' is the homomorphism density and ''p'' the edge density. Its corollaries state that tensor powers make the ratio arbitrarily small, and that there are ''p'' in (0, 1) and a nonconstant graphon ''W'' with edge density ''p'' and ''H''-density ''p''<sup>66</sup>, so that ''H'' is a connected bipartite graph with a cycle that is not forcing.
* ''Method, as described:'' every pair of points of the triple system lies in exactly two triples, which turns a local sign constraint into a four-incidence correlation. A kernel built from symmetric matrices of half rank over a large finite field, with determinant signs of the induced quotient forms, realizes a negative correlation. Color-refinement scores make the intended type assignment dominate, a crossed product gives a symmetric kernel, and the contribution of singular point differences is bounded through Lagrangian intersection profiles. A finite host graph is then sampled from the kernel.
* '''Source.''' The manuscript [https://github.com/openai/math/tree/1581d4cbdd69a0faf34b2089614fe2a814316a6a/preprints/A-counterexample-to-Sidorenkos-conjecture-September-23-2026 A counterexample to Sidorenko's conjecture].
* '''Formalization, as described by the repository.''' The scope note [https://github.com/openai/math/blob/1581d4cbdd69a0faf34b2089614fe2a814316a6a/lean/docs/161.md lean/docs/161.md] states that the formalization constructs, for the fixed 35-vertex graph, a nonempty finite simple host graph violating Sidorenko's inequality, and that the forcing-conjecture consequence is outside this statement. The Comparator statement is [https://github.com/openai/math/blob/1581d4cbdd69a0faf34b2089614fe2a814316a6a/lean/ComparatorChallenges/SidorenkoCounterexample.lean SidorenkoCounterexample.lean].
* '''Catalogue status.''' Google DeepMind's Formal Conjectures project records <code>sidorenko_conjecture</code> as research solved (false), with a formal-proof link to the collection's Lean development, and states that the finite counterexample also refutes the graphon form ([https://github.com/google-deepmind/formal-conjectures/blob/197f7f8dcc457f556754f826389d2ec7a0d85b92/FormalConjectures/Wikipedia/SidorenkoConjecture.lean FormalConjectures/Wikipedia/SidorenkoConjecture.lean], checked 18 October 2026 at commit <code>197f7f8</code>). The change was made by [https://github.com/google-deepmind/formal-conjectures/pull/6898 pull request 6898], merged 11 October 2026, which marked several problems solved by the collection.

== Public follow-up work ==
{| class="wikitable"
! Date !! Work !! Relation !! Public claim !! Public status (checked 18 October 2026)
|-
| 2026-10-08 || [https://github.com/mathvet/mathvet MathVet] (GitHub, review of openai/math, tables at repository commit <code>c76f1e4</code>, 14 October 2026) || Review (fidelity of the formal statements) || Rates the family "partial", calls the Lean statement "a faithful Sidorenko counterexample" with homomorphism counts that include noninjective maps, and records a sandboxed Comparator pass. The forcing-conjecture claim has no Lean statement, and the counts 35 and 66 and connectivity are properties of the defined graph rather than stated. || MathVet states that its ratings concern whether the Lean states the headline claims.
|-
| 2026-10-09 || [https://github.com/rohanarun/sidorenko-template-refinements/tree/5ca68cb81cfcd7f1b32102b93e186b2b51d5e2f8 rohanarun/sidorenko-template-refinements] (GitHub) || Extension within the method (conditional) || A computer-assisted enumeration of sphere triangulations shows that 35 vertices is the minimum within the manuscript's finite construction template, and a counting step gets a smaller constant. The README states that this is not a minimum over all counterexamples or a smaller general counterexample. || Described by its README as an independent AI-generated research draft prepared with Codex.
|-
| 2026-10-10 to 2026-10-14 || [https://github.com/leanprover/con-leche/blob/90577d9e49ee3aed45da3d421bdf5dc780192304/DESIGN.md con-leche development journal] (task #348) || Verification (second kernel) || In its run over all Comparator challenges of the collection at commit <code>fd4aeeb</code>, the journal's table of exceptions does not list <code>SidorenkoCounterexample</code>, so this challenge was accepted by con-leche and by Lean's official kernel. || Development journal.
|-
| 2026-10-12 || [https://github.com/erebos-labs/sidorenko-sharp-coercivity/tree/64f9ebf631c568c86adfdd3e1b6d8249cca00d8d erebos-labs/sidorenko-sharp-coercivity] (GitHub, release v1.1.0) || Extension of one step (relaxation) || Sharp coercivity constants 1/40 and 1/48 on a real relaxation of one step of the construction, with exact certificates. || Described by the repository as an AI-assisted project.
|-
| 2026-10-14 || [https://hexagonmath.org/2610.00241v1 Hexagon 2610.00241v1], ''A six-spin obstruction to antiferromagnetic biclique maximization'' || Related work || Disproves a conjecture of Sah, Sawhney, Stoner and Zhao on partition functions of spin models with one positive eigenvalue, by a six-spin model on a triangle with three pendant edges. Its bibliography cites the OpenAI manuscript, in the version accessed on 11 October 2026. || Hexagon preprint, version 1.
|-
| 2026-10-16 || J. Jardine, Lattice24, [https://github.com/JJardine919/openai-math-audit/blob/a06a8c6e77974d4c6021338a55a8e91b634f67f7/reviews/rank_468.json referee review] in [https://github.com/JJardine919/openai-math-audit JJardine919/openai-math-audit] (archived at [https://doi.org/10.5281/zenodo.23422995 Zenodo 10.5281/zenodo.23422995]) || Review (AI-assisted audit) || The referee review reports no gap and no issues after reading every section. It states that it machine-checked the triple system, including that each of the 33 point pairs lies in exactly two faces and that color refinement is discrete on all 35 vertices, and that it checked the reduction, the transverse section and the sampling constants step by step. || Part of an audit of the collection's manuscripts that the audit describes as complete. The reviews are published under CC BY 4.0.
|}

== Notes ==
* The list covers follow-ups found in public sources up to the date above; it is not a priority or completeness claim.

[[Category:OpenAI results]]

Sidorenko's conjecture - Revision history

Aftermath bot: New page for the counterexample to Sidorenko's conjecture and the forcing conjecture with public follow-ups