  An Isabelle/HOL formalisation of G\"odel's two incompleteness theorems is
presented. The work follows \'Swierczkowski's detailed proof of the theorems
using hereditarily finite (HF) set theory. Avoiding the usual arithmetical
encodings of syntax eliminates the necessity to formalise elementary number
theory within an embedded logical calculus. The Isabelle formalisation uses two
separate treatments of variable binding: the nominal package is shown to scale
to a development of this complexity, while de Bruijn indices turn out to be
ideal for coding syntax. Critical details of the Isabelle proof are described,
in particular gaps and errors found in the literature.
