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 KoutsoukouArgyraki.
A longstanding 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ösMilner, 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 KoutsoukouArgyraki.
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:
Note that exdirectory lists are not shown.
