Formal Verification of the Empty Hexagon Number

TL;DR

The paper formalizes the reduction used to prove the finite empty hexagon number $h(6)=30$ into Lean, bridging discrete geometry and propositional logic via triple orientations. It develops a canonical-position symmetry-breaking framework and a detailed CNF encoding φ_n whose unsatisfiability for $n=30$ yields the geometric result. By relying on a verified SAT-checking pipeline (LRAT proofs and cake_lpr), the work strengthens trust in computer-assisted proofs within Erdős–Szekeres-type problems. The contribution also provides a reusable framework for connecting geometric objects to SAT assignments, paving the way for formally verifying future SAT-based discrete geometry results.

Abstract

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 $φ_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ő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.

Figures (9)

• Figure 1: Illustration of the proof for . The left subfigure shows how a point in $S \setminus s$ that lies inside $s$ will be inside one of the triangles induced by the convex hull of $s$ (orange triangle). The right subfigure shows how if the $\textsf{ConvexPoints}$ predicate does not hold of $s$, then some point $a \in s$ will be inside one of the triangles induced by the convex hull of $s \setminus \{a\}$.
• Figure 2: Illustration of triple orientations, where $\sigma(p, r, q) = -1, \sigma(r, s, q) = 1,$ and $\sigma(p, s, t) = 0$.
• Figure 3: Illustration for $\sigma(p,q,r) = 1 \; \land \; \sigma(q,r,s) = 1 \implies \sigma(p, r, s) = 1$. As we have assumptions $\theta_3 > \theta_2 > \theta_4$ by the forward direction of the slope-orientation equivalence, we deduce $\theta_3 > \theta_4$, and then conclude $\sigma(p, r, s) = 1$ by the backward direction of the slope-orientation equivalence.
• Figure 4: The pointsets depicted in \ref{['fig:equiv-a', 'fig:equiv-b']} are $\sigma$-equivalent with since the bijection $f$ defined by $(a,b,c,d) \mapsto (b', d', c', a')$ satisfies $\sigma(p_i, p_j, p_k) = \sigma(f(p_i), f(p_j), f(p_j))$ for every $\{p_i, p_j, p_k\} \subseteq \{a,b,c,d\}$. On the other hand, no orientation-preserving bijection exists for \ref{['fig:equiv-c', 'fig:equiv-d']}, which are only $\sigma$-equivalent with .
• Figure 5: Illustration of the proof of the symmetry breaking theorem. Note that the highlighted holes are preserved as $\sigma$-equivalence is preserved. For simplicity we have omitted the illustration of the Lex order property.

Theorems & Definitions (2)

• Theorem
• Definition 1: Canonical Position