Challenge 4: Sidorenko's conjecture for bipartite graphs with sides of size at most $r$

Definition

TenChallenges_Challenge_04

by utkuokur · Nov 4, 2026 · Mathlib 0df444a (Lean v4.33.1)

graph-theorysidorenkoten-challenges

The scaled form of Challenge 4. For a natural number $r$ , $\mathrm{Sid}(r)$ says: for every finite graph $H$ which is bipartite with both sides of size at most $r$ , and every finite graph $G$ with at least one vertex,

t(H,G)\ \ge\ t(K_2,G)^{\,e(H)}.

Here $t$ is the homomorphism density and $e(H)$ the number of edges of $H$ . The rungs $r\le 4$ follow from Sidorenko's theorem for bipartite graphs with at most four vertices on one side; the rung $r=22$ is refuted by OpenAI's 2026 counterexample ( $H$ with sides $13$ and $22$ ); the rungs $5\le r\le 21$ are open.

Formalization Note. Vertex types of $H$ and $G$ range over finite types in the lowest universe; the host graph is required to be nonempty.

Definition code

import Definitions.Def_TenChallenges_Sidorenko

open SimpleGraph

namespace TenChallenges

/-- Sidorenko's inequality for bipartite graphs with at most `r` vertices in each side. -/
def statement_04 (r : ℕ) : Prop :=
  ∀ {W V : Type} [Fintype W] [Fintype V] [Nonempty V]
    (H : SimpleGraph W) (G : SimpleGraph V),
    BipartiteBoundedBy H r → SidorenkoFor H G

end TenChallenges

Source

Ten Challenges repository, file Challenges/challenge_04.lean (commit ff14a56), https://github.com/TenChallenges/ten-challenges/blob/main/Challenges/challenge_04.lean; V. Bajpai, N. Bowler, J. Carmesin, U. Okur, 10 Scalable Challenges in Combinatorics, AI4Math @ CICM 2026, challenge 4.

Read-back

What the Lean code literally says, in plain math · claude-fable-5-1

Definition statement_04 $r$ . For a natural number $r$ (the only parameter, and $r = 0$ is allowed), statement_04 $r$ is the following proposition.

For all types $W$ and $V$ (both in the lowest type universe), for every finiteness structure on $W$ and every finiteness structure on $V$ (so $W$ and $V$ are finite sets of vertices, and the claim is asserted for each way of witnessing finiteness), under the assumption that $V$ is nonempty, for every simple graph $H$ on $W$ (a symmetric, irreflexive adjacency relation $\sim_H$ ) and every simple graph $G$ on $V$ (adjacency $\sim_G$ ): if $H$ is bipartite with sides bounded by $r$ , meaning there exist subsets $X, Y \subseteq W$ with

$X \cap Y = \varnothing$ ,
for all $v, w \in W$ : $v \sim_H w$ implies ( $v \in X$ and $w \in Y$ ) or ( $v \in Y$ and $w \in X$ ),
$X \cup Y = W$ ,
$|X| \le r$ and $|Y| \le r$ ,

then

t(H,G) \;\ge\; t(K_2,G)^{\,e(H)} ,

where $t(H,G)$ is the real number

t(H,G) = \frac{\#\{\, f : W \to V \;\mid\; \forall\, a, b \in W,\ a \sim_H b \Rightarrow f(a) \sim_G f(b) \,\}}{|V|^{\,|W|}}

(the number of all functions $W \to V$ sending $H$ -adjacent pairs to $G$ -adjacent pairs — not required injective — divided by $|V|$ to the power $|W|$ ), $K_2$ is the complete graph on a two-element vertex set $\{0,1\}$ , so that

t(K_2,G) = \frac{\#\{\, f : \{0,1\} \to V \mid f(0) \sim_G f(1) \,\}}{|V|^2} = \frac{\#\{(u,v) \in V \times V : u \sim_G v\}}{|V|^2} = \frac{2\,|E(G)|}{|V|^2},

and $e(H)$ is the number of edges of $H$ (unordered pairs $\{a,b\}$ with $a \sim_H b$ ), used as a natural-number exponent, so the right-hand side is $1$ when $e(H) = 0$ even if $t(K_2,G) = 0$ . The inequality is non-strict.

Edge cases silently included. Since $V$ is nonempty, $|V| \ge 1$ and no division by zero occurs in either density. Since $W$ is finite, $|X|$ and $|Y|$ are true cardinalities (the convention "infinite set has cardinality $0$ " built into the side bound does not come into play), and any $H$ meeting the hypothesis has $|W| \le 2r$ . $W$ may be empty: then $H$ is the graph with no vertices, the hypothesis holds with $X = Y = \varnothing$ for every $r$ , and the conclusion reads $1 \ge 1$ . If $r = 0$ the hypothesis forces $W = \varnothing$ . If $H$ has no edges, every function is a homomorphism and the conclusion reads $1 \ge 1$ . If $G$ has no edges and $H$ has at least one edge, the right-hand side is $0$ and the conclusion is $t(H,G) \ge 0$ . Nothing requires $H$ to be connected, to have both sides nonempty, to have $|X|$ or $|Y|$ equal to $r$ , or to be the complete bipartite graph; $G$ is an arbitrary finite simple graph on a nonempty vertex set (not required to be bipartite, regular, dense, or related to $H$ in any way).

Human review

Endorsed by Shuze Chen · Nov 4, 2026
Confirmed by the moderator at approval.
Endorsed by utkuokur · Nov 4, 2026
Confirmed by the mission captain (proposal self-audit).

View graph

Challenge 4: Sidorenko's conjecture for bipartite graphs with sides of size at most rrr

Challenge 4: Sidorenko's conjecture for bipartite graphs with sides of size at most $r$