Formalising New Mathematics in Isabelle: Diagonal Ramsey
Fuente:
arXiv
Saved in:
| Main Author: | |
|---|---|
| Format: | Preprint |
| Published: |
2025
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866913655910563840 |
|---|---|
| author | Paulson, Lawrence C |
| author_facet | Paulson, Lawrence C |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2501_10852 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Formalising New Mathematics in Isabelle: Diagonal Ramsey Paulson, Lawrence C Logic in Computer Science Combinatorics 05D10, 03B35, 68V15, 68V20 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. |
| title | Formalising New Mathematics in Isabelle: Diagonal Ramsey |
| topic | Logic in Computer Science Combinatorics 05D10, 03B35, 68V15, 68V20 |
| url | https://arxiv.org/abs/2501.10852 |