Sidorenko's conjecture asserts that every finite bipartite graph 
with at least one graph edge and every nonempty finite simple graph 
satisfy
 |
where 
is the graph homomorphism density and
is the complete graph on two vertices.
Thus the bound counts arbitrary adjacency-preserving maps,
rather than only injective copies.
The inequality is established for trees, even cycle graphs, complete
bipartite graphs, and hypercube graphs (Conlon
and Lee 2021). A graph satisfying it for every 
is called a Sidorenko graph
(Zhao 2023). The 5-Möbius ladder, obtained
by deleting a Hamiltonian cycle from 
, is a classical test case (Zhao 2023).
OpenAI (2026, p. 1) announced a counterexample using the Sidorenko incidence graph 
, which has 35 vertices
and 66 edges. The argument proves that some finite simple graph 
with a graph edge satisfies
 |
The 35 vertices belong to the pattern 
, and the argument does not specify a small host 
. The release attributes the construction and proof
to an internal OpenAI model and supplies a Lean formalization of this finite-host
statement. MathVet (2026) reports successful independent kernel checking of the formalized
theorem. Its accompanying statement review is model-assisted
and remains pre-referee.
