Lawrence Paulson (Cambridge)

Formalising Erdős and Larson: Ordinal Partition Theory

Note date and time change: Tue 11am

A number of results in infinitary combinatorics have been formalised in the proof assistant Isabelle/HOL. These include results on ordinal partition relations by Erdős–Milner, Specker, Larson and Nash-Williams, leading to Larson’s 1973 proof that for all $m$ in $ℕ$, $ω^ω → (ω^ω,m)$. This material is available online; here we discuss some of the most challenging aspects of the formalisation process, and wider issues in the formalisation of research-grade mathematics. See also the paper in Experimental Mathematics 31:2, 2022.