2026-08-17T19:55:30Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:24616 2025-12-12T15:10:00Z ddc:004 open_access

Formalising New Mathematics in Isabelle: Diagonal Ramsey Paulson, Lawrence C. Isabelle formalisation of mathematics Ramsey’s theorem computer algebra 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Lawrence C. Paulson 2025 Is Part Of LIPIcs, Volume 352, 16th International Conference on Interactive Theorem Proving (ITP 2025) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.ITP.2025.18 urn:nbn:de:0030-drops-246163 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2025.18 eng https://creativecommons.org/licenses/by/4.0/legalcode