← All papers
A New Upper Bound for the Turán Density of the Tetrahedron
math.CO
Sep 23, 2026 · v1
cs.DM math.OC
TL;DR
A complete formal proof in Lean 4 verifies the flag-algebra certificate establishing the improved Turán density upper bound for the tetrahedron.
Abstract
We prove that the Turán density of the tetrahedron $K_4^{(3)}$ satisfies $π(K_4^{(3)}) \le 312372062889819/560000000000000 < 0.557808$, improving Baber's upper bound of $0.5615$ and closing about $62\%$ of the gap to the conjectured value $5/9$. The proof uses an exact seven-vertex flag-algebra certificate incorporating degree-stationarity from Razborov's differential method. To find the certificate, we combine the established techniques of cutting planes and column generation to optimize jointly over flag families whose types have at most five vertices. We give a complete formal proof of this Turán density bound in Lean 4.
Problem
Turán's tetrahedron problem asks for the Turán density of the complete 3-uniform hypergraph on four vertices, conjectured to be 5/9. Prior upper bounds left a substantial gap to this conjectured value.
Approach
An exact seven-vertex flag-algebra certificate is constructed, incorporating degree-stationarity from Razborov's differential method. To find the certificate, cutting planes and column generation are combined to optimize jointly over flag families whose types have at most five vertices. The resulting Turán density bound is given a complete formal proof in Lean 4.
Results
The Turán density satisfies π(K_4^(3)) ≤ 312372062889819/560000000000000 < 0.557808, improving Baber's bound of 0.5615 and closing about 62% of the gap to the conjectured 5/9.