A Formalised Theorem in the Partition Calculus

A paper on ordinal partitions by Erd\H{o}s and Milner (1972) has been formalised using the proof assistant Isabelle/HOL, augmented with a library for Zermelo-Fraenkel set theory. The work is part of a project on formalising the partition calculus. The chosen material is particularly appropriate in view of the substantial corrections later published by its authors, illustrating the potential value of formal verification.