Document Open Access Logo

An End-To-End Verification of Keller’s Conjecture

Authors James Gallicchio , Cayden Codel , Jeremy Avigad , Marijn J. H. Heule

PDF

File

Thumbnail PDF
PDF
LIPIcs.ITP.2026.26.pdf
  • Filesize: 1.21 MB
  • 20 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation → Logic and verification
  • Mathematics of computing → Graph theory
Keywords
  • Keller’s conjecture
  • the Lean theorem prover
  • SAT encodings
  • SAT solving
  • Trestle
  • formal verification

Metrics

Abstract

In 1930, Keller conjectured that every gap-free tiling of ℝⁿ by n-dimensional unit cubes must contain cubes that fully share an (n - 1)-dimensional face. Keller’s conjecture holds for n ≤ 7 and fails for n ≥ 8. The final case, n = 7, was settled in 2020 using a mix of traditional and automated reasoning. The result was obtained by reducing the conjecture to a set of clique-existence problems, encoding those problems into propositional logic, breaking symmetries, and solving them with a SAT solver.
In this paper, we present an end-to-end verification in Lean 4 of Keller’s conjecture for all dimensions. First, we simplify a prior reduction of Keller’s conjecture to the clique-existence problems. We then verify an improved SAT encoding of those problems, as well as some symmetry reasoning on the encoding. Throughout our work, we sought to maximize the synergy between interactive and automated techniques while minimizing human proof burden. In particular, the symmetry reasoning was split between Lean and a mechanically-checkable proof system, since neither was suitable on their own for verifying all of the symmetry reasoning. We discuss how and why we chose to split the reasoning across these systems based on their relative strengths and weaknesses.

Cite As Get BibTex

James Gallicchio, Cayden Codel, Jeremy Avigad, and Marijn J. H. Heule. An End-To-End Verification of Keller’s Conjecture. In 17th International Conference on Interactive Theorem Proving (ITP 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 382, pp. 26:1-26:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026) https://doi.org/10.4230/LIPIcs.ITP.2026.26

Author Details

James Gallicchio
  • Carnegie Mellon University, Pittsburgh, PA, USA
Cayden Codel
  • Carnegie Mellon University, Pittsburgh, PA, USA
Jeremy Avigad
  • Carnegie Mellon University, Pittsburgh, PA, USA
Marijn J. H. Heule
  • Carnegie Mellon University, Pittsburgh, PA, USA

Funding

This research was partially supported by the DARPA https://www.darpa.mil/research/programs/expmath-exponential-mathematics through DARPA CMO contract number HR0011262E028, by the NSF https://www.nsf.gov/funding/opportunities/aiming-artificial-intelligence-formal-methods-mathematical through NSF Grant DMS-2434614, and by the https://www.cmu.edu/hoskinson/.

Supplementary Materials

References

  1. F.A. Aloul, I.L. Markov, and K.A. Sakallah. Shatter: efficient symmetry-breaking for boolean satisfiability. In Proceedings 2003. Design Automation Conference (IEEE Cat. No.03CH37451), pages 836-839, 2003. URL: https://doi.org/10.1145/775832.776042.
  2. Markus Anders, Cayden R. Codel, and Marijn J. H. Heule. Orbitopal fixing in SAT. In Sebastian Junges and Guy Katz, editors, Tools and Algorithms for the Construction and Analysis of Systems - 32nd International Conference, TACAS 2026, Held as Part of the International Joint Conferences on Theory and Practice of Software, ETAPS 2026, Turin, Italy, April 11-16, 2026, Proceedings, Part I, Lecture Notes in Computer Science, pages 89-109. Springer, 2026. URL: https://doi.org/10.1007/978-3-032-22752-2_5.
  3. Zachary Battleman, Joseph E. Reeves, and Marijn J. H. Heule. Problem Partitioning via Proof Prefixes. In Jeremias Berg and Jakob Nordström, editors, 28th International Conference on Theory and Applications of Satisfiability Testing (SAT 2025), volume 341 of Leibniz International Proceedings in Informatics (LIPIcs), pages 3:1-3:18, Dagstuhl, Germany, 2025. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. URL: https://doi.org/10.4230/LIPIcs.SAT.2025.3.
  4. Armin Biere, Tobias Faller, Katalin Fazekas, Mathias Fleury, Nils Froleyks, and Florian Pollitt. CaDiCaL 2.0. In Arie Gurfinkel and Vijay Ganesh, editors, Computer Aided Verification - 36th International Conference, CAV 2024, Montreal, QC, Canada, July 24-27, 2024, Proceedings, Part I, volume 14681 of Lecture Notes in Computer Science, pages 133-152. Springer, 2024. URL: https://doi.org/10.1007/978-3-031-65627-9_7.
  5. Armin Biere, Marijn Heule, Hans van Maaren, and Toby Walsh, editors. Handbook of Satisfiability - Second Edition, volume 336 of Frontiers in Artificial Intelligence and Applications. IOS Press, 2021. URL: https://doi.org/10.3233/FAIA336.
  6. Joshua Brakensiek, Marijn Heule, John Mackey, and David Narváez. The Resolution of Keller’s Conjecture. Journal of Automated Reasoning, 66(3):277-300, 2022. URL: https://doi.org/10.1007/s10817-022-09623-5.
  7. Curtis Bright, Kevin K. H. Cheung, Brett Stevens, Ilias Kotsireas, and Vijay Ganesh. A SAT-based resolution of Lam’s Problem. Proceedings of the AAAI Conference on Artificial Intelligence, 35(5):3669-3676, May 2021. URL: https://doi.org/10.1609/aaai.v35i5.16483.
  8. Sam Buss and Neil Thapen. DRAT and propagation redundancy proofs without new variables. Logical Methods in Computer Science, Volume 17, Issue 2, April 2021. URL: https://doi.org/10.23638/LMCS-17(2:12)2021.
  9. Joshua Clune. A Formalized Reduction of Keller’s Conjecture. In Proceedings of the 12th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2023, pages 90-101, New York, NY, USA, 2023. Association for Computing Machinery. URL: https://doi.org/10.1145/3573105.3575669.
  10. Cayden R. Codel, Jeremy Avigad, and Marijn J. H. Heule. Verified Encodings for SAT Solvers. In 2023 Formal Methods in Computer-Aided Design (FMCAD), pages 141-151, 2023. ISSN: 2708-7824. URL: https://doi.org/10.34727/2023/isbn.978-3-85448-060-0_22.
  11. Cayden R. Codel, Marijn J. H. Heule, and Jeremy Avigad. Verified substitution redundancy checking. In Nina Narodytska and Philipp Rümmer, editors, Proceedings of the 24th Conference on Formal Methods in Computer-Aided Design - FMCAD 2024, volume 5 of Formal Methods in Computer-Aided Design, pages 186-196, Vienna, Austria, October 2024. TU Wien Academic Press. URL: https://doi.org/10.34727/2024/isbn.978-3-85448-065-5_24.
  12. K. Corrádi and S. Szabó. A combinatorial approach for Keller’s conjecture. Periodica Mathematica Hungarica, 21(2):95-100, 1990. URL: https://doi.org/10.1007/BF01946848.
  13. Luís Cruz-Filipe, Marijn J. H. Heule, Warren A. Hunt, Matt Kaufmann, and Peter Schneider-Kamp. Efficient certified RAT verification. In Leonardo De Moura, editor, Automated Deduction - CADE 26, volume 10395, pages 220-236. Springer International Publishing, Cham, 2017. URL: https://doi.org/10.1007/978-3-319-63046-5_14.
  14. 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, 2019. URL: https://doi.org/10.1007/S10817-018-9490-4.
  15. Jennifer Debroni, John D. Eblen, Michael A. Langston, Wendy Myrvold, Peter Shor, and Dinesh Weerapurage. A complete resolution of the Keller maximum clique problem. In Proceedings of the Twenty-Second Annual ACM-SIAM Symposium on Discrete Algorithms, pages 129-135. Society for Industrial and Applied Mathematics, January 2011. URL: https://doi.org/10.1137/1.9781611973082.11.
  16. Sofia Giljegård and Johan Wennerbreck. Puzzle solving with proof. Master’s thesis, Chalmers University of Technology, University of Gothenburg, 2021. Google Scholar
  17. Stephan Gocht and Jakob Nordström. Certifying parity reasoning efficiently using pseudo-boolean proofs. In Thirty-Fifth AAAI Conference on Artificial Intelligence, AAAI 2021, Thirty-Third Conference on Innovative Applications of Artificial Intelligence, IAAI 2021, The Eleventh Symposium on Educational Advances in Artificial Intelligence, EAAI 2021, Virtual Event, February 2-9, 2021, pages 3768-3777. AAAI Press, 2021. URL: https://doi.org/10.1609/AAAI.V35I5.16494.
  18. Marijn J. H. Heule, Oliver Kullmann, and Victor W. Marek. Solving and verifying the Boolean Pythagorean triples problem via cube-and-conquer. In Nadia Creignou and Daniel Le Berre, editors, Theory and Applications of Satisfiability Testing - SAT 2016, pages 228-245, Cham, 2016. Springer International Publishing. URL: https://doi.org/10.1007/978-3-319-40970-2_15.
  19. Marijn J. H. Heule, Oliver Kullmann, Siert Wieringa, and Armin Biere. Cube and conquer: Guiding CDCL SAT solvers by lookaheads. In Kerstin Eder, João Lourenço, and Onn Shehory, editors, Hardware and Software: Verification and Testing, pages 50-65, Berlin, Heidelberg, 2012. Springer Berlin Heidelberg. Google Scholar
  20. Marijn J. H. Heule and Manfred Scheucher. Happy ending: An empty hexagon in every set of 30 points. In Tools and Algorithms for the Construction and Analysis of Systems: 30th International Conference, TACAS 2024, pages 61-80, Berlin, Heidelberg, 2024. Springer-Verlag. URL: https://doi.org/10.1007/978-3-031-57246-3_5.
  21. Andrzej P. Kisielewicz. Rigid polyboxes and Keller’s conjecture, 2014. arXiv:1304.1639 [math]. URL: https://doi.org/10.48550/arXiv.1304.1639.
  22. Andrzej P. Kisielewicz and Magdalena Łysakowska. On Keller’s Conjecture in Dimension Seven. The Electronic Journal of Combinatorics, 22(1):P1.16, 2015. URL: https://doi.org/10.37236/4153.
  23. Jeffrey C. Lagarias and Peter W. Shor. Keller’s cube-tiling conjecture is false in high dimensions. Bull. Amer. Math. Soc. (N.S.), 1992. Publisher: arXiv Version Number: 1. URL: https://doi.org/10.48550/arXiv.MATH/9210222.
  24. Mackey. A Cube Tiling of Dimension Eight with No Facesharing. Discrete & Computational Geometry, 28(2):275-279, August 2002. URL: https://doi.org/10.1007/s00454-002-2801-9.
  25. Joao Marques-Silva and Inês Lynce. Towards robust CNF encodings of cardinality constraints. In Christian Bessière, editor, Principles and Practice of Constraint Programming - CP 2007, pages 483-497, Berlin, Heidelberg, 2007. Springer Berlin Heidelberg. Google Scholar
  26. The Mathlib Community. The Lean mathematical library. In Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, POPL '20, January 2020. URL: https://doi.org/10.1145/3372885.3373824.
  27. Ross M. McConnell, Kurt Mehlhorn, Stefan Näher, and Pascal Schweitzer. Certifying algorithms. Comput. Sci. Rev., 5(2):119-161, 2011. URL: https://doi.org/10.1016/J.COSREV.2010.09.009.
  28. Leonardo de Moura and Sebastian Ullrich. The Lean 4 theorem prover and programming language. In Automated Deduction - CADE 28, pages 625-635, 2021. URL: https://doi.org/10.1007/978-3-030-79876-5_37.
  29. Van-Hau Nguyen, Van-Quyet Nguyen, Kyungbaek Kim, and Pedro Barahona. Empirical study on SAT-encodings of the at-most-one constraint. In The 9th International Conference on Smart Media and Applications, SMA 2020, pages 470-475, New York, NY, USA, 2021. Association for Computing Machinery. URL: https://doi.org/10.1145/3426020.3426170.
  30. Oskar Perron. Über lückenlose Ausfüllung desn-dimensionalen Raumes durch kongruente Würfel. Mathematische Zeitschrift, 46(1):1-26, December 1940. URL: https://doi.org/10.1007/BF01181421.
  31. 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 (TACAS), pages 389-406, Cham, 2023. Springer Nature Switzerland. URL: https://doi.org/10.1007/978-3-031-30823-9_20.
  32. 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), volume 309 of Leibniz International Proceedings in Informatics (LIPIcs), pages 35:1-35:19, 2024. URL: https://doi.org/10.4230/LIPIcs.ITP.2024.35.
  33. S. Szabó. A reduction of Keller’s conjecture. Periodica Mathematica Hungarica, 17(4):265-277, December 1986. URL: https://doi.org/10.1007/BF01848388.
  34. 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, 2023. URL: https://doi.org/10.1007/s10009-022-00690-y.
  35. 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, volume 8561, pages 422-429. Springer International Publishing, 2014. URL: https://doi.org/10.1007/978-3-319-09284-3_31.
  36. Magdalena Łysakowska. Extended Keller graph and its properties. Quaestiones Mathematicae, 42(4):551-560, April 2019. URL: https://doi.org/10.2989/16073606.2018.1462865.
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

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