Formal Verification of the Empty Hexagon Number
Bernardo Subercaseaux, Wojciech Nawrocki, James Gallicchio, Cayden Codel, Mario Carneiro, Marijn J. H. Heule
cs.CG
Mar 26, 2024 · v1
TL;DR
Formalizes in Lean the SAT-based proof that the empty hexagon number h(6) equals 30.
Abstract
A recent breakthrough in computer-assisted mathematics showed that every set of 30 points in the plane in general position 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 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.
Problem
The empty hexagon number problem (showing every set of 30 points in general position contains an empty convex hexagon) was resolved computationally using 17300 CPU hours of SAT solving, but the resulting proof was not formally verified.
Approach
The paper formally verifies the computational proof in Lean. The original approach constructed a CNF formula whose unsatisfiability implies no point set avoids an empty convex hexagon, then used a SAT solver to find an unsatisfiability proof. The formal verification checks both the geometric reduction (that unsatisfiability of the formula implies the mathematical theorem) and the SAT proof certificate, connecting the computer-assisted argument to a machine-checked theorem in Lean.
Results
The formal verification in Lean confirms that every set of 30 points in the plane in general position contains an empty convex hexagon, closing the gap between the computational proof and a formally verified result. The verification handles the O(n^4)-clause formula construction and validates the SAT solver's unsatisfiability certificate.
