![[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 25 May 2023, 17:00-18:00
Formalising Erdős and Larson: Ordinal Partition Theory
- 👤 Speaker: Professor Lawrence C. Paulson FRS (University of Cambridge) 🔗 Website
- 📅 Date & Time: Thursday 25 May 2023, 17:00 - 18:00
- 📍 Venue: Centre for Mathematical Sciences MR12, CMS
Abstract
A long-standing question in mathematics is the relevance of formalisation to practice. Rising awareness of fallibility among mathematicians suggests formalisation as a remedy. But are today’s proof assistants up to the task? And what is the right formalism?
A wide variety of mathematical topics have been formalised in simple type theory using Isabelle/HOL. The partition calculus was introduced by Erdős and R. Rado in 1956 as the study of “analogues and extensions of Ramsey’s theorem”. Highly technical results were obtained by Erdös-Milner, Specker and Larson (among many others) for the case of ordinal partition relations, which is concerned with countable ordinals and order types. Much of this material was formalised recently, with the assistance of Džamonja and Koutsoukou-Argyraki.
Some highlights of this work will be presented along with general observations about role of type theory in the formalisation of mathematics.
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
- Centre for Mathematical Sciences MR12, CMS
- 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
- School of Physical Sciences
- School of Technology
- Trust & Technology Initiative - interesting events
- yk449
Note: Ex-directory lists are not shown.