发表机构
School of Computing, KAIST; School of Computational Sciences, Korea Institute for Advanced Study (KIAS); Center for Artificial Intelligence and Natural Sciences, Korea Institute for Advanced Study (KIAS)（KAIST计算机学院; 韩国高等研究院计算科学学院; 韩国高等研究院人工智能与自然科学中心）
机构由 AI 辅助整理，请以论文原文为准。AI 中文总结
本研究证明四面体Turán密度上界改进至0.557808，缩小与猜想值差距62%，采用旗代数证书与割平面、列生成联合优化，并在Lean 4中形式化验证。
AI 中文摘要
我们证明了四面体$K_4^{(3)}$的Turán密度满足$π(K_4^{(3)}) \le 312372062889819/560000000000000 < 0.557808$，改进了Baber的0.5615上界，并缩小了与猜想值$5/9$之间约62%的差距。证明使用了精确的七顶点旗代数证书，该证书结合了Razborov微分方法中的度平稳性。为找到该证书，我们将割平面法和列生成法这两种成熟技术相结合，对类型至多包含五个顶点的旗族进行联合优化。我们在Lean 4中给出了该Turán密度界的完整形式化证明。
英文摘要
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.
Comments28 pages, 5 figures, 8 tables. v2: Slightly improved upper bound and updated exact certificate following continuation of the search to convergence. Lean 4 formalization, exact certificate and code: https://github.com/taeyool/tetrahedron-turan
