Document Open Access Logo

Formalising New Mathematics in Isabelle: Diagonal Ramsey

Author Lawrence C. Paulson

PDF HTML 5

Files

Thumbnail PDF
PDF
LIPIcs.ITP.2025.18.pdf
  • Filesize: 1.55 MB
  • 18 pages
HTML5 Logo HTML (experimental)
LIPIcs.ITP.2025.18.html

Document Identifiers

Related Versions

Subject Classification

ACM Subject Classification
  • Theory of computation → Logic and verification
  • Mathematics of computing → Combinatorics
  • Computing methodologies → Symbolic and algebraic manipulation
Keywords
  • Isabelle
  • formalisation of mathematics
  • Ramsey’s theorem
  • computer algebra

Metrics

Abstract

The formalisation of mathematics is becoming routine, but its value to research mathematicians remains unproven. There are few examples of using proof assistants to verify new work. This paper reports the formalisation - inspired by a Lean one by Bhavik Mehta - of a major new result [Marcelo Campos et al., 2023] about Ramsey numbers. One unexpected finding was a heavy role for computer algebra techniques.

Cite As Get BibTex

Lawrence C. Paulson. Formalising New Mathematics in Isabelle: Diagonal Ramsey. In 16th International Conference on Interactive Theorem Proving (ITP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 352, pp. 18:1-18:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025) https://doi.org/10.4230/LIPIcs.ITP.2025.18

Author Details

Lawrence C. Paulson
  • Computer Laboratory, University of Cambridge, UK

Acknowledgements

Many thanks to Mantas Baksys, Simon Griffiths, Bhavik Mehta and Andrew Thomason for mathematical advice. Simon provided a detailed plan for fixing the proofs of lemma 9.1 and 10.1, while Andrew sketched a probabilistic proof of the lower bound for Ramsey numbers. Help with specialised Isabelle proof methods was provided by Manuel Eberl (real_asymp) and Fabian Immler (approximation). Sophie Tourret and Bhavik read a draft of the paper and provided detailed, thoughtful comments; thanks also to the referees and the PC chairs.

Supplementary Materials

References

  1. Vigleik Angeltveit and Brendan D. McKay. R(5,5) ≤ 46, 2024. URL: https://arxiv.org/abs/2409.15709.
  2. Clemens Ballarin. Exploring the structure of an algebra text with locales. Journal of Automated Reasoning, 64(6):1093-1121, 2020. URL: https://doi.org/10.1007/s10817-019-09537-9.
  3. Clemens Ballarin and Lawrence C. Paulson. A pragmatic approach to extending provers by computer algebra - with applications to coding theory. Fundamenta Informaticae, 39:1-20, 1999. URL: https://doi.org/10.3233/FI-1999-391201.
  4. Marcelo Campos, Simon Griffiths, Robert Morris, and Julian Sahasrabudhe. An exponential improvement for diagonal Ramsey, 2023. URL: https://arxiv.org/abs/2303.09521.
  5. Manuel Eberl. Verified real asymptotics in Isabelle/HOL. In James Davenport and Dongming Wang, editors, International Symposium on Symbolic and Algebraic Computation (ISAAC 2019), pages 147-154. ACM, 2019. URL: https://doi.org/10.1145/3326229.3326240.
  6. Chelsea Edmonds. Undirected graph theory. Archive of Formal Proofs, September 2022. , Formal proof development. URL: https://isa-afp.org/entries/Undirected_Graph_Theory.html.
  7. Chelsea Edmonds, Angeliki Koutsoukou-Argyraki, and Lawrence C. Paulson. Formalising Szemerédi’s regularity lemma and Roth’s theorem on arithmetic progressions in Isabelle/HOL. Journal of Automated Reasoning, 67(1), 2023. URL: https://doi.org/10.1007/s10817-022-09650-2.
  8. Chelsea Edmonds and Lawrence C. Paulson. Formal probabilistic methods for combinatorial structures using the Lovász local lemma. In Brigitte Pientka and Sandrine Blazy, editors, 13th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2024, pages 132-146. Association for Computing Machinery, 2024. URL: https://doi.org/10.1145/3636501.3636946.
  9. Thibault Gauthier and Chad E. Brown. A formal proof of R(4,5)=25. In Yves Bertot, Temur Kutsia, and Michael Norrish, editors, 15th International Conference on Interactive Theorem Proving (ITP 2024), volume 309 of Leibniz International Proceedings in Informatics (LIPIcs), pages 16:1-16:18. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2024. URL: https://doi.org/10.4230/LIPIcs.ITP.2024.16.
  10. Georges Gonthier, Andrea Asperti, Jeremy Avigad, Yves Bertot, Cyril Cohen, François Garillot, Stéphane Le Roux, Assia Mahboubi, Russell O'Connor, Sidi Ould Biha, Ioana Pasca, Laurence Rideau, Alexey Solovyev, Enrico Tassi, and Laurent Théry. A machine-checked proof of the odd order theorem. In Sandrine Blazy, Christine Paulin-Mohring, and David Pichardie, editors, Interactive Theorem Proving, LNCS 7998, pages 163-179. Springer, 2013. URL: https://doi.org/10.1007/978-3-642-39634-2_14.
  11. Charles M Grinstead and Sam M Roberts. On the Ramsey numbers R(3, 8) and R(3, 9). Journal of Combinatorial Theory, Series B, 33(1):27-51, 1982. URL: https://doi.org/10.1016/0095-8956(82)90055-7.
  12. Johannes Hölzl. Proving inequalities over reals with computation in Isabelle/HOL. In Gabriel Dos Reis and Laurent Théry, editors, ACM SIGSAM 2009 International Workshop on Programming Languages for Mechanized Mathematics Systems (PLMMS'09), pages 38-45, 2009. Google Scholar
  13. Johannes Hölzl, Fabian Immler, and Brian Huffman. Type classes and filters for mathematical analysis in Isabelle/HOL. In Sandrine Blazy, Christine Paulin-Mohring, and David Pichardie, editors, ITP, LNCS 7998, pages 279-294. Springer, 2013. URL: https://doi.org/10.1007/978-3-642-39634-2_21.
  14. Tobias Nipkow. A tutorial introduction to structured Isar proofs. Online documentation. URL: http://isabelle.in.tum.de/dist/Isabelle/doc/isar-overview.pdf.
  15. Lawrence C. Paulson. Large-scale formal proof for the working mathematician - lessons learnt from the ALEXANDRIA project. In Intelligent Computer Mathematics (CICM 2023), pages 3-15. Springer, 2023. URL: https://doi.org/10.1007/978-3-031-42753-4_1.
  16. Lawrence C. Paulson. An exponential improvement for diagonal Ramsey. Archive of Formal Proofs, September 2024. , Formal proof development. URL: https://isa-afp.org/entries/Diagonal_Ramsey.html.
  17. Lawrence C. Paulson. A formalised theorem in the partition calculus. Annals of Pure and Applied Logic, 175(1, Part B):103246, 2024. Kenneth Kunen (1943-2020). URL: https://doi.org/10.1016/j.apal.2023.103246.
  18. Clark Weissman. Lisp 1.5 Primer. Dickenson Publishing Company, 1967. Google Scholar
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-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact