Formalising New Mathematics in Isabelle: Diagonal Ramsey
Lawrence C Paulson
TL;DR
This paper demonstrates the formalisation of a new mathematical result on Ramsey numbers in Isabelle, highlighting the role of computer algebra techniques in formal verification of novel mathematical work.
Contribution
It presents the first formal proof of a recent, significant result in Ramsey theory, showcasing the integration of computer algebra in formal proof systems.
Findings
Formal proof of a new Ramsey number result in Isabelle
Identification of the importance of computer algebra techniques in formalising new mathematics
Validation of recent mathematical discoveries through formal methods
Abstract
The formalisation of mathematics is starting to become routine, but the value of this technology to the work of mathematicians remains to be shown. There are few examples of using proof assistants to verify brand-new work. This paper reports the formalisation of a major new result (arXiv:2303.09521) about Ramsey numbers that was announced in 2023. One unexpected finding was the heavy need for computer algebra techniques.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.