# Counterexamples to Sidorenko’s conjecture and the forcing conjecture

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

- [A counterexample to Sidorenko's conjecture](../../preprints/A-counterexample-to-Sidorenkos-conjecture-September-23-2026/paper.pdf)

## 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](../ComparatorChallenges/SidorenkoCounterexample.lean) |