New upper bound found for tetrahedron Turán density problem
A New Upper Bound for the Turán Density of the Tetrahedron
Discrete Mathematics
Summary
The paper studies a mathematical problem about how densely a certain pattern called a tetrahedron can appear in a large 3-dimensional network. The authors improve the known upper limit on this density, bringing it closer to a long-standing conjecture. They use advanced mathematical tools and computer-assisted proof techniques to achieve this improvement and provide a fully formalized proof.
What this means in practice
- •For network designers: Understand constraints on 3-uniform hypergraph density patterns to better design complex interconnected systems.
- •For formal verification engineers: Use the Lean 4 formal proof framework as a model for verifying complex combinatorial properties in software and hardware systems.
A theory result. No direct application yet.
Authors
Gyeongwon Jeong, Seonghun Park, Seonghyuk Im, Joonkyung Lee, Hongseok Yang
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.