Formalising (part of) the Diagonal Ramsey Paper

Add to your list(s) Download to your calendar using vCal

• Professor Lawrence Paulson (University of Cambridge)
• Thursday 07 March 2024, 17:00-18:00
• MR14 Centre for Mathematical Sciences.

If you have a question about this talk, please contact Anand Rao Tadipatri.

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

This talk is part of the Formalisation of mathematics with interactive theorem provers series.

This talk is included in these lists:

• All CMS events
• All Talks (aka the CURE list)
• CMS Events
• Cambridge talks
• DPMMS Lists
• DPMMS Pure Maths study groups
• DPMMS info aggregator
• DPMMS lists
• Department of Computer Science and Technology talks and seminars
• Formalisation of mathematics with interactive theorem provers
• Hanchen DaDaDash
• Interested Talks
• MR14 Centre for Mathematical Sciences
• School of Physical Sciences
• School of Technology
• Trust & Technology Initiative - interesting events
• bld31

Note that ex-directory lists are not shown.