  This is an overview of a formalisation project in the proof assistant
Isabelle/HOL of a number of research results in infinitary combinatorics and
set theory (more specifically in ordinal partition relations) by
Erd\H{o}s--Milner, Specker, Larson and Nash-Williams, leading to Larson's proof
of the unpublished result by E.C. Milner asserting that for all $m \in
\mathbb{N}$, $\omega^\omega\arrows(\omega^\omega, m)$. This material has been
recently formalised by Paulson and is available on the Archive of Formal
Proofs; here we discuss some of the most challenging aspects of the
formalisation process. This project is also a demonstration of working with
Zermelo-Fraenkel set theory in higher-order logic.
