Document Open Access Logo

A Formal Proof of R(4,5)=25

Authors Thibault Gauthier , Chad E. Brown

PDF
Thumbnail PDF

File

LIPIcs.ITP.2024.16.pdf
  • Filesize: 0.8 MB
  • 18 pages

Document Identifiers

Author Details

Thibault Gauthier
  • Czech Technical University in Prague, Czech Republic
Chad E. Brown
  • Czech Technical University in Prague, Czech Republic

Funding

Both authors were supported by the Ministry of Education, Youth and Sports within the dedicated program ERC CZ under the project POSTMAN no. LL1902. The second author has also received funding from the European Union’s Horizon Europe research and innovation programme under grant agreement no. 101070254 CORESENSE.

Cite AsGet BibTex

Thibault Gauthier and Chad E. Brown. A Formal Proof of R(4,5)=25. In 15th International Conference on Interactive Theorem Proving (ITP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 309, pp. 16:1-16:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
https://doi.org/10.4230/LIPIcs.ITP.2024.16

Abstract

In 1995, McKay and Radziszowski proved that the Ramsey number R(4,5) is equal to 25. Their proof relies on a combination of high-level arguments and computational steps. The authors have performed the computational parts of the proof with different implementations in order to reduce the possibility of an error in their programs. In this work, we prove this theorem in the interactive theorem prover HOL4 limiting the uncertainty to the small HOL4 kernel. Instead of verifying their algorithms directly, we rely on the HOL4 interface to MiniSat to prove gluing lemmas. To reduce the number of such lemmas and thus make the computational part of the proof feasible, we implement a generalization algorithm. We verify that its output covers all the possible cases by implementing a custom SAT-solver extended with a graph isomorphism checker.

Subject Classification

ACM Subject Classification
  • Theory of computation → Automated reasoning
Keywords
  • Ramsey numbers
  • SAT solvers
  • symmetry breaking
  • generalization
  • HOL4

Metrics

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

Related Versions

References

  1. Vigleik Angeltveit and Brendan D. McKay. R(5, 5) ≤ 48. J. Graph Theory, 89(1):5-13, 2018. URL: https://doi.org/10.1002/JGT.22235.
  2. Vigleik Angeltveit, Brendan D. McKay, and Stanislaw P. Radziszowski. Website section: All maximal Ramsey(4,5)-graphs. https://users.cecs.anu.edu.au/~bdm/data/ramsey.html, 2016. Accessed on May 26, 2024.
  3. Kenneth I Appel and Wolfgang Haken. Every planar map is four colorable, volume 98. American Mathematical Soc., 1989. Google Scholar
  4. Yves Bertot. A short presentation of Coq. In Otmane Ait Mohamed, César Muñoz, and Sofiène Tahar, editors, Conference on Theorem Proving in Higher Order Logics (TPHOLs), volume 5170 of LNCS, pages 12-16. Springer, 2008. URL: http://doi.org/10.1007/978-3-540-71067-7_3.
  5. Béla Bollobás. Modern Graph Theory, volume 184 of Graduate Texts in Mathematics. Springer, 2002. URL: https://doi.org/10.1007/978-1-4612-0619-4.
  6. Michael Codish, Michael Frank, Avraham Itzhakov, and Alice Miller. Computing the Ramsey number R(4, 3, 3) using abstraction and symmetry breaking. Constraints An Int. J., 21(3):375-393, 2016. URL: https://doi.org/10.1007/S10601-016-9240-3.
  7. 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.
  8. Martin Davis and Hilary Putnam. A computing procedure for quantification theory. J. ACM, 7(3):201-215, 1960. URL: https://doi.org/10.1145/321033.321034.
  9. Niklas Eén and Niklas Sörensson. An extensible SAT-solver. In Enrico Giunchiglia and Armando Tacchella, editors, Theory and Applications of Satisfiability Testing, 6th International Conference, SAT 2003. Santa Margherita Ligure, Italy, May 5-8, 2003 Selected Revised Papers, volume 2919 of Lecture Notes in Computer Science, pages 502-518. Springer, 2003. URL: https://doi.org/10.1007/978-3-540-24605-3_37.
  10. Thibault Gauthier and Chad E. Brown. Software accompanying the paper "A formal proof of R(4,5)=25". https://github.com/barakeel/ramsey, 2024. Accessed on May 26, 2024.
  11. Georges Gonthier. Formal proof the four-color theorem. Notices of the AMS, 55(11):1382-1393, 2008. URL: http://www.ams.org/notices/200811/tx081101382p.pdf.
  12. Thomas C. Hales, Mark Adams, Gertrud Bauer, Dat Tat Dang, John Harrison, Truong Le Hoang, Cezary Kaliszyk, Victor Magron, Sean McLaughlin, Thang Tat Nguyen, Truong Quang Nguyen, Tobias Nipkow, Steven Obua, Joseph Pleso, Jason M. Rute, Alexey Solovyev, An Hoai Thi Ta, Trung Nam Tran, Diep Thi Trieu, Josef Urban, Ky Khac Vu, and Roland Zumkeller. A formal proof of the Kepler conjecture. CoRR, abs/1501.02155, 2015. URL: https://arxiv.org/abs/1501.02155.
  13. Thomas C. Hales and Samuel P. Ferguson. A formulation of the Kepler conjecture. Discret. Comput. Geom., 36(1):21-69, 2006. URL: https://doi.org/10.1007/S00454-005-1211-1.
  14. John Harrison. HOL Light: An overview. In Stefan Berghofer, Tobias Nipkow, Christian Urban, and Makarius Wenzel, editors, Conference on Theorem Proving in Higher Order Logics (TPHOLs), volume 5674 of LNCS, pages 60-66. Springer, 2009. URL: https://doi.org/10.1007/978-3-642-03359-9_4.
  15. 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 - 19th International Conference, Bordeaux, France, July 5-8, 2016, Proceedings, volume 9710 of Lecture Notes in Computer Science, pages 228-245. Springer, 2016. URL: https://doi.org/10.1007/978-3-319-40970-2_15.
  16. JG Kalbfleisch. Construction of special edge-chromatic graphs. Canadian Mathematical Bulletin, 8(5):575-584, 1965. Google Scholar
  17. Brendan D. McKay and Adolfo Piperno. Practical graph isomorphism, II. J. Symb. Comput., 60:94-112, 2014. URL: https://doi.org/10.1016/J.JSC.2013.09.003.
  18. Brendan D. McKay and Stanislaw P. Radziszowski. R(4, 5) = 25. J. Graph Theory, 19(3):309-322, 1995. URL: https://doi.org/10.1002/JGT.3190190304.
  19. Konrad Slind and Michael Norrish. A brief overview of HOL4. In Otmane Aït Mohamed, César A. Muñoz, and Sofiène Tahar, editors, Conference on Theorem Proving in Higher Order Logics (TPHOLs), volume 5170 of LNCS, pages 28-32. Springer, 2008. URL: https://doi.org/10.1007/978-3-540-71067-7_6.
  20. Tjark Weber and Hasan Amjad. Efficiently checking propositional refutations in HOL theorem provers. J. Appl. Log., 7(1):26-40, 2009. URL: https://doi.org/10.1016/J.JAL.2007.07.003.
  21. Nathan Wetzler, Marijn Heule, and Warren A. Hunt Jr. 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 - 17th International Conference, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 14-17, 2014. Proceedings, volume 8561 of Lecture Notes in Computer Science, pages 422-429. Springer, 2014. URL: https://doi.org/10.1007/978-3-319-09284-3_31.
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact