University of Cambridge > > Formalisation of mathematics with interactive theorem provers  > Formalising Erdős and Larson: Ordinal Partition Theory

Formalising Erdős and Larson: Ordinal Partition Theory

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

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.

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.


© 2006-2023, University of Cambridge. Contact Us | Help and Documentation | Privacy and Publicity