Date:
Thursday, 7 March, 2024 - 17:00 to 18:00
Speaker:
Professor Lawrence Paulson (University of Cambridge)
Venue:
MR14 Centre for Mathematical Sciences
Last March, a paper appeared on arXiv announcing a dramatic advance in Ramsey theory: an exponential reduction in the upper bound for Ramsey numbers. Last November, Bhavik Mehta announced that he had formalised the paper (in Lean), even before the referees had finished checking it. This talk describes a partial formalisation of the same paper within Isabelle. It includes a quick review of Ramsey's theorem, an outline of the paper and comments on the mathematics therein, and some notes on the formalisation itself.
---
WATCH ONLINE HERE: https://www.microsoft.com/en-gb/microsoft-teams/join-a-meeting?rtc=1 Meeting ID: 370 771 279 261 Passcode: iCo7a5
Seminar series:
Formalisation of mathematics with interactive theorem provers
