{"id":"palomar/PALOMAR-2026-10-13-000012","url":"https://github.com/xliu2022/improved-sidorenko-lean/tree/ba6f109bf01436ca15e55fdf5d35dbea85ffd9c9","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-10-13-000012-v1.json","repo":"https://github.com/xliu2022/improved-sidorenko-lean","tags":["math.CO","msc:05C65","msc:05C35","msc:05D40","extremal-combinatorics","hypergraphs","turan-density","lean"],"score":0,"title":"Improved Sidorenko bound for hypergraph Turán densities","trust":"high","domain":"math.CO","source":"palomar","authors":["Xizhi Liu"],"reviews":0,"subject":"math.CO","summary":"For every finite simple r-uniform hypergraph F with r >= 3 and m >= 1 edges, the Turán density is at most 1-c_r/m^((r-1)/r), where c_r=(1/(4r^2))(4/r)^(1/r)(1-1/r)^(2-2/r). The formalization proves the finite embedding argument using two potentials and the Lovász Local Lemma, constructs the extremal numbers, and proves the existence of their binomial-normalized limit by vertex deletion and double counting.","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-10-13","reactions":{},"formalized":true,"formalizes":[{"title":"Improved Sidorenko bound for hypergraph Turán densities","identifier":"","relationship":"formalizes"},{"title":"On a graph-problem of Turán","identifier":"","relationship":"formalizes"}]}