![[Search]](/static/images/search.gif){kind=small}
![[A-Z Index]](/static/images/az.gif){kind=small}
![[Contact]](/static/images/contact.gif){kind=small}
![[University of Cambridge]](/static/images/identifier2.gif){kind=small}
![[Talks.cam]](/static/images/talkslogosmall.gif)
Thursday 07 March 2024, 17:00-18:00
Formalising (part of) the Diagonal Ramsey Paper
- đ¤ Speaker: Professor Lawrence Paulson (University of Cambridge)
- đ Date & Time: Thursday 07 March 2024, 17:00 - 18:00
- đ Venue: MR14 Centre for Mathematical Sciences
Abstract
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
Series This talk is part of the Formalisation of mathematics with interactive theorem provers series.
Included in Lists
- All CMS events
- All Talks (aka the CURE list)
- bld31
- Cambridge talks
- CMS Events
- Department of Computer Science and Technology talks and seminars
- DPMMS info aggregator
- DPMMS lists
- DPMMS Lists
- DPMMS Pure Maths study groups
- Formalisation of mathematics with interactive theorem provers
- Hanchen DaDaDash
- Interested Talks
- Martin's interesting talks
- MR14 Centre for Mathematical Sciences
- School of Physical Sciences
- School of Technology
- Trust & Technology Initiative - interesting events
- yk449
Note: Ex-directory lists are not shown.