A New Upper Bound for the Turán Density of the Tetrahedron
Gyeongwon Jeong, Seonghun Park, Seonghyuk Im, Joonkyung Lee, Hongseok Yang
math.CO
Sep 23, 2026 · v2
cs.DM math.OC
TL;DR
Gives a complete formal proof in Lean 4 of the new upper bound on the Turán density of the tetrahedron, verifying the flag-algebra certificate.
Abstract
We prove that the Turán density of the tetrahedron $K_4^{(3)}$ satisfies $π(K_4^{(3)}) \le 14993367693127837/26880000000000000 < 0.557789$, 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 conjectured that the Turán density of the 3-uniform tetrahedron K_4^(3) equals 5/9. The best known upper bound was Baber's 0.5615.
Approach
An exact seven-vertex flag-algebra certificate is built that also uses degree-stationarity from Razborov's differential method. The certificate is found by solving a semidefinite program through a sequence of linear programs, combining cutting planes and column generation over flag families with types of up to five vertices. The resulting Turán density bound is formally proved in Lean 4.
Results
The bound π(K_4^(3)) < 0.557789 is proved, closing about 62% of the gap between Baber's bound and 5/9. In experiments, combining cutting planes and column generation gave the strongest bounds, and adding five-root types improved the bounds further.
