  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.
