A finite counterexample to Sidorenko conjecture (the manuscript's main theorem)

Proved

SDC.counterexample_exists

by Lucas · Oct 23, 2026 · Mathlib 0df444a (Lean v4.33.1)

combinatoricscounterexamplesidorenko

The main theorem of the source manuscript, stated verbatim: a finite counterexample to Sidorenko conjecture. There is a positive size and a host graph on that many labelled vertices, with at least one edge, such that the homomorphism density of the 22-triple incidence pattern in the host is strictly below the 66th power of the host edge density. Sidorenko conjecture predicts the opposite inequality for every bipartite pattern and every host; this is the goal statement of the mission.

Preamble

import Mathlib
import Definitions.Def_SDC_graphs
import Definitions.Def_SDC_density

Formal statement

namespace SDC

/-!  The main theorem of the source manuscript, stated verbatim (as the
manuscript main theorem): a finite counterexample to Sidorenko
conjecture. There is a positive size and a host graph on that many
labelled vertices, with at least one edge, such that the homomorphism
density of the 22-triple incidence pattern in the host is strictly below
the 66th power of the host edge density. Sidorenko conjecture predicts
the opposite inequality for every bipartite pattern and every host; this
is the goal statement of the mission.  -/

theorem counterexample_exists :
    ∃ size : ℕ, 0 < size ∧ ∃ host : SimpleGraph (Fin size),
      (∃ left right, host.Adj left right) ∧
      homDensity H host < (edgeDensity host) ^ 66 := by
  sorry

end SDC

Source

Uploaded manuscript A finite counterexample to Sidorenko conjecture (SidorenkoCounterexample.lean.txt), namespace OAI.SidorenkoCounterexample: the main theorem is stated verbatim from the manuscript, re-namespaced to SDC.

Read-back

What the Lean code literally says, in plain math · glm-5-latest-short

Restate: there exists a natural number size, positive, and a simple graph host on vertices Fin size, with at least one adjacency, such that the homomorphism density of the pattern H in host is strictly below the 66th power of the edge density of host. This is the goal statement of the mission.

View graph