Document Open Access Logo

Formal Verification of the Empty Hexagon Number

Authors Bernardo Subercaseaux , Wojciech Nawrocki , James Gallicchio , Cayden Codel , Mario Carneiro , Marijn J. H. Heule

PDF
Thumbnail PDF

File

LIPIcs.ITP.2024.35.pdf
  • Filesize: 0.86 MB
  • 19 pages

Document Identifiers

Author Details

Bernardo Subercaseaux
  • Carnegie Mellon University, Pittsburgh, PA, USA
Wojciech Nawrocki
  • Carnegie Mellon University, Pittsburgh, PA, USA
James Gallicchio
  • Carnegie Mellon University, Pittsburgh, PA, USA
Cayden Codel
  • Carnegie Mellon University, Pittsburgh, PA, USA
Mario Carneiro
  • Carnegie Mellon University, Pittsburgh, PA, USA
Marijn J. H. Heule
  • Carnegie Mellon University, Pittsburgh, PA, USA

Funding

Supported by the National Science Foundation (NSF) grant CCF-2229099.

Cite As Get BibTex

Bernardo Subercaseaux, Wojciech Nawrocki, James Gallicchio, Cayden Codel, Mario Carneiro, and Marijn J. H. Heule. Formal Verification of the Empty Hexagon Number. In 15th International Conference on Interactive Theorem Proving (ITP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 309, pp. 35:1-35:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024) https://doi.org/10.4230/LIPIcs.ITP.2024.35

Abstract

A recent breakthrough in computer-assisted mathematics showed that every set of 30 points in the plane in general position (i.e., no three points on a common line) contains an empty convex hexagon. Heule and Scheucher solved this problem with a combination of geometric insights and automated reasoning techniques by constructing CNF formulas ϕ_n, with O(n⁴) clauses, such that if ϕ_n is unsatisfiable then every set of n points in general position must contain an empty convex hexagon. An unsatisfiability proof for n = 30 was then found with a SAT solver using 17 300 CPU hours of parallel computation. In this paper, we formalize and verify this result in the Lean theorem prover. Our formalization covers ideas in discrete computational geometry and SAT encoding techniques by introducing a framework that connects geometric objects to propositional assignments. We see this as a key step towards the formal verification of other SAT-based results in geometry, since the abstractions we use have been successfully applied to similar problems. Overall, we hope that our work sets a new standard for the verification of geometry problems relying on extensive computation, and that it increases the trust the mathematical community places in computer-assisted proofs.

Subject Classification

ACM Subject Classification
  • Theory of computation → Logic and verification
Keywords
  • Empty Hexagon Number
  • Discrete Computational Geometry
  • Erdős-Szekeres

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Supplementary Materials

References

  1. A. Biere, M. Heule, H. van Maaren, and T. Walsh. Handbook of Satisfiability: Volume 185 Frontiers in Artificial Intelligence and Applications. IOS Press, NLD, 2009. Google Scholar
  2. Joshua Brakensiek, Marijn Heule, John Mackey, and David Narváez. The Resolution of Keller’s Conjecture, 2023. URL: https://arxiv.org/abs/1910.03740.
  3. Curtis Bright, Kevin K. H. Cheung, Brett Stevens, Ilias S. Kotsireas, and Vijay Ganesh. A SAT-based resolution of Lam’s Problem. In Thirty-Fifth AAAI Conference on Artificial Intelligence, AAAI 2021, pages 3669-3676. AAAI Press, 2021. URL: https://doi.org/10.1609/AAAI.V35I5.16483.
  4. Shawn T. Brown, Paola Buitrago, Edward Hanna, Sergiu Sanielevici, Robin Scibek, and Nicholas A. Nystrom. Bridges-2: A Platform for Rapidly-Evolving and Data Intensive Research, pages 1-4. Association for Computing Machinery, New York, NY, USA, 2021. Google Scholar
  5. Davide Castelvecchi. Mathematicians welcome computer-assisted proof in 'grand unification' theory. Nature, 595(7865):18-19, June 2021. URL: https://doi.org/10.1038/d41586-021-01627-2.
  6. Cayden Codel, Marijn J. H. Heule, and Jeremy Avigad. Verified Encodings for SAT Solvers. In Alexander Nadel and Kristin Yvonne Rozier, editors, Proceedings of the 23rd conference on Formal Methods In Computer-Aided Design, 2023. Google Scholar
  7. James Crawford, Matthew Ginsberg, Eugene Luks, and Amitabha Roy. Symmetry-breaking predicates for search problems. In Proc. KR'96, 5th Int. Conf. on Knowledge Representation and Reasoning, pages 148-159. Morgan Kaufmann, 1996. Google Scholar
  8. Luís Cruz-Filipe, João Marques-Silva, and Peter Schneider-Kamp. Formally Verifying the Solution to the Boolean Pythagorean Triples Problem. J. Autom. Reason., 63(3):695-722, October 2019. URL: https://doi.org/10.1007/s10817-018-9490-4.
  9. Luís Cruz-Filipe and Peter Schneider-Kamp. Formally Proving the Boolean Pythagorean Triples Conjecture. In Thomas Eiter and David Sands, editors, LPAR-21. 21st International Conference on Logic for Programming, Artificial Intelligence and Reasoning, volume 46 of EPiC Series in Computing, pages 509-522. EasyChair, 2017. URL: https://doi.org/10.29007/jvdj.
  10. Leonardo de Moura, Soonho Kong, Jeremy Avigad, Floris van Doorn, and Jakob von Raumer. The Lean Theorem Prover (System Description). In Amy P. Felty and Aart Middeldorp, editors, Automated Deduction - CADE-25, pages 378-388, Cham, 2015. Springer International Publishing. Google Scholar
  11. Théo Delemazure, Tom Demeulemeester, Manuel Eberl, Jonas Israel, and Patrick Lederer. Strategyproofness and proportionality in party-approval multiwinner elections. In Brian Williams, Yiling Chen, and Jennifer Neville, editors, Thirty-Seventh AAAI Conference on Artificial Intelligence, AAAI 2023, Thirty-Fifth Conference on Innovative Applications of Artificial Intelligence, IAAI 2023, Thirteenth Symposium on Educational Advances in Artificial Intelligence, EAAI 2023, Washington, DC, USA, February 7-14, 2023, pages 5591-5599. AAAI Press, 2023. URL: https://doi.org/10.1609/AAAI.V37I5.25694.
  12. Paul Erdős and George Szekeres. On some extremum problems in elementary geometry. Ann. Univ. Sci. Budapest. Eötvös Sect. Math., 3(4):53-62, 1960. Google Scholar
  13. Paul Erdős and György Szekeres. A combinatorial problem in geometry. Compositio Mathematica, 2:463-470, 1935. URL: http://eudml.org/doc/88611.
  14. Stefan Felsner and Helmut Weil. Sweeps, arrangements and signotopes. Discrete Applied Mathematics, 109(1):67-94, April 2001. URL: https://doi.org/10.1016/S0166-218X(00)00232-8.
  15. Tobias Gerken. Empty Convex Hexagons in Planar Point Sets. Discrete & Computational Geometry, 39(1):239-272, March 2008. URL: https://doi.org/10.1007/s00454-007-9018-x.
  16. Sofia Giljegård and Johan Wennerbeck. Puzzle Solving with Proof. Master’s thesis, Chalmers University of Technology, 2021. Google Scholar
  17. W. T. Gowers, Ben Green, Freddie Manners, and Terence Tao. On a conjecture of Marton, 2023. URL: https://arxiv.org/abs/2311.05762.
  18. Andrew Haberlandt, Harrison Green, and Marijn J. H. Heule. Effective auxiliary variables via structured reencoding. In 26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023), volume 271 of Leibniz International Proceedings in Informatics (LIPIcs), pages 11:1-11:19, Dagstuhl, Germany, 2023. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. URL: https://doi.org/10.4230/LIPIcs.SAT.2023.11.
  19. Heiko Harborth. Konvexe Fünfecke in ebenen Punktmengen. Elemente der Mathematik, 33:116-118, 1978. URL: http://eudml.org/doc/141217.
  20. Marijn J. H. Heule, Oliver Kullmann, and Victor W. Marek. Solving and Verifying the Boolean Pythagorean Triples Problem via Cube-and-Conquer, pages 228-245. Springer International Publishing, 2016. URL: https://doi.org/10.1007/978-3-319-40970-2_15.
  21. Marijn J. H. Heule and Manfred Scheucher. Happy ending: An empty hexagon in every set of 30 points, 2024. URL: https://arxiv.org/abs/2403.00737.
  22. Andreas F Holmsen, Hossein Nassajian Mojarrad, János Pach, and Gábor Tardos. Two extensions of the erdős-szekeres problem. arXiv preprint arXiv:1710.11415, 2017. Google Scholar
  23. J. D. Horton. Sets with No Empty Convex 7-Gons. Canadian Mathematical Bulletin, 26(4):482-484, 1983. URL: https://doi.org/10.4153/CMB-1983-077-8.
  24. Donald E. Knuth. Axioms and Hulls. In Donald E. Knuth, editor, Axioms and Hulls, Lecture Notes in Computer Science, pages 1-98. Springer, Berlin, Heidelberg, 1992. URL: https://doi.org/10.1007/3-540-55611-7_1.
  25. Boris Konev and Alexei Lisitsa. A SAT Attack on the Erdos Discrepancy Conjecture, 2014. URL: https://arxiv.org/abs/1402.2184.
  26. Peter Lammich. Efficient Verified (UN)SAT Certificate Checking. Journal of Automated Reasoning, 64(3):513-532, March 2020. URL: https://doi.org/10.1007/s10817-019-09525-z.
  27. Filip Marić. Formal verification of a modern SAT solver by shallow embedding into Isabelle/HOL. Theor. Comput. Sci., 411(50):4333-4356, 2010. URL: https://doi.org/10.1016/J.TCS.2010.09.014.
  28. Filip Marić. Fast formal proof of the Erdős-Szekeres conjecture for convex polygons with at most 6 points. J. Autom. Reason., 62(3):301-329, 2019. URL: https://doi.org/10.1007/S10817-017-9423-7.
  29. The mathlib Community. The Lean mathematical library. In Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, POPL ’20. ACM, January 2020. URL: https://doi.org/10.1145/3372885.3373824.
  30. Carlos M. Nicolas. The Empty Hexagon Theorem. Discrete & Computational Geometry, 38(2):389-397, September 2007. URL: https://doi.org/10.1007/s00454-007-1343-6.
  31. Duckki Oe, Aaron Stump, Corey Oliver, and Kevin Clancy. Versat: A Verified Modern SAT Solver. In Viktor Kuncak and Andrey Rybalchenko, editors, Verification, Model Checking, and Abstract Interpretation, pages 363-378, Berlin, Heidelberg, 2012. Springer Berlin Heidelberg. Google Scholar
  32. Manfred Scheucher. Two disjoint 5-holes in point sets. Computational Geometry, 91:101670, December 2020. URL: https://doi.org/10.1016/j.comgeo.2020.101670.
  33. Sarek Høverstad Skotåm. CreuSAT, Using Rust and Creusot to create the world’s fastest deductively verified SAT solver. Master’s thesis, University of Oslo, 2022. URL: https://www.duo.uio.no/handle/10852/96757.
  34. Leila Sloman. `A-Team' of Math Proves a Critical Link Between Addition and Sets. https://www.quantamagazine.org/a-team-of-math-proves-a-critical-link-between-addition-and-sets-20231206/, December 2023. Google Scholar
  35. Bernardo Subercaseaux and Marijn J. H. Heule. The Packing Chromatic Number of the Infinite Square Grid is 15. In Sriram Sankaranarayanan and Natasha Sharygina, editors, Tools and Algorithms for the Construction and Analysis of Systems - 29th International Conference, TACAS 2023, Held as Part of ETAPS 2022, Proceedings, Part I, volume 13993 of Lecture Notes in Computer Science, pages 389-406. Springer, 2023. URL: https://doi.org/10.1007/978-3-031-30823-9_20.
  36. Bernardo Subercaseaux, John Mackey, Marijn J. H. Heule, and Ruben Martins. Minimizing pentagons in the plane through automated reasoning, 2023. URL: https://arxiv.org/abs/2311.03645.
  37. Bernardo Subercaseaux, Wojciech Nawrocki, James Gallicchio, Cayden Codel, Mario Carneiro, and Marijn J. H. Heule. EmptyHexagonLean. Software, (visited on 2024-08-23). URL: https://github.com/bsubercaseaux/EmptyHexagonLean/tree/itp2024
    Software Heritage Logo archived version
    full metadata available at: https://doi.org/10.4230/artifacts.22467
  38. Andrew Suk. On the erdős-szekeres convex polygon problem. Journal of the American Mathematical Society, 30(4):1047-1053, 2017. Google Scholar
  39. George Szekeres and Lindsay Peters. Computer solution to the 17-point Erdős-Szekeres problem. The ANZIAM Journal, 48(2):151-164, 2006. URL: https://doi.org/10.1017/S144618110000300X.
  40. George Szekeres and Lindsay Peters. Computer solution to the 17-point erdős-szekeres problem. The ANZIAM Journal, 48(2):151-164, 2006. Google Scholar
  41. Yong Kiam Tan, Marijn J. H. Heule, and Magnus O. Myreen. Verified Propagation Redundancy and Compositional UNSAT Checking in CakeML. International Journal on Software Tools for Technology Transfer, 25(2):167-184, April 2023. URL: https://doi.org/10.1007/s10009-022-00690-y.
  42. Mark Walters. It Appears That Four Colors Suffice : A Historical Overview of the Four-Color Theorem, 2004. URL: https://api.semanticscholar.org/CorpusID:14382286.
  43. Nathan Wetzler, Marijn J. H. Heule, and Warren A. Hunt. DRAT-trim: Efficient checking and trimming using expressive clausal proofs. In Carsten Sinz and Uwe Egly, editors, Theory and Applications of Satisfiability Testing - SAT 2014, pages 422-429, Cham, 2014. Springer International Publishing. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact