Formalising Erdős and Larson: Ordinal Partition Theory

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

• Professor Lawrence C. Paulson FRS (University of Cambridge)
• Thursday 25 May 2023, 17:00-18:00
• Centre for Mathematical Sciences MR12, CMS.

If you have a question about this talk, please contact Angeliki Koutsoukou-Argyraki.

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.

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

This talk is included in these lists:

• Centre for Mathematical Sciences MR12, CMS
• 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
• School of Physical Sciences
• School of Technology
• Trust & Technology Initiative - interesting events
• bld31

Note that ex-directory lists are not shown.