A recent breakthrough in computer-assisted mathematics showed that every set of $30$ points in the plane in general position (i.e., without three on a common line) contains an empty convex hexagon, thus closing a line of research dating back to the 1930s. Through a combination of geometric insights and automated reasoning techniques, Heule and Scheucher constructed a CNF formula $\phi_n$, with $O(n^4)$ clauses, whose unsatisfiability implies that no set of $n$ points in general position can avoid an empty convex hexagon. An unsatisfiability proof for n = 30 was then found with a SAT solver using 17300 CPU hours of parallel computation, thus implying that the empty hexagon number h(6) is equal to 30. In this paper, we formalize and verify this result in the Lean theorem prover. Our formalization covers discrete computational geometry ideas and SAT encoding techniques that have been successfully applied to similar Erd\H{o}s-Szekeres-type problems. In particular, our framework provides tools to connect standard mathematical objects to propositional assignments, which represents a key step towards the formal verification of other SAT-based mathematical results. Overall, we hope that this work sets a new standard for verification when extensive computation is used for discrete geometry problems, and that it increases the trust the mathematical community has in computer-assisted proofs in this area.

翻译：近期计算机辅助数学领域的一项突破性成果表明，平面中任意30个处于一般位置（即无三点共线）的点集必然包含一个空凸六边形，从而终结了可追溯至20世纪30年代的研究脉络。通过几何洞察与自动化推理技术的结合，Heule与Scheucher构建了包含$O(n^4)$个子句的CNF公式$\phi_n$，其不可满足性意味着不存在n个处于一般位置的点可避免产生空凸六边形。他们利用SAT求解器经过17300 CPU小时的并行计算，获得了n=30时的不可满足性证明，从而得出空六边形数h(6)=30。本文在Lean定理证明器中对该结果进行了形式化验证。我们的形式化工作涵盖了离散计算几何思想与SAT编码技术，这些方法已成功应用于类似的Erdős–Szekeres型问题。特别地，我们的框架建立了标准数学对象与命题赋值之间的衔接工具，这为其他基于SAT的数学成果的形式化验证奠定了关键基础。我们期望这项研究能为涉及大规模计算的离散几何问题建立新的验证标准，并增强数学界对该领域计算机辅助证明的信任度。