# A Mechanised Proof of G"odel's Incompleteness Theorems using Nominal Isabelle

arXiv: https://arxiv.org/abs/2104.13792 · HTML: https://mlsanity.com/paper/2104.13792/

## Key facts

- Cited by 2 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 28 Apr 2021.

## Built on by (most cited first, 2 of 2)

- [HybridProver: Augmenting Theorem Proving with LLM-Driven Proof Synthesis and Refinement](https://mlsanity.com/paper/2505.15740/) (2025)
- [IsabeLLM: Automated Theorem Proving Applied to Formally Verifying Consensus](https://mlsanity.com/paper/2606.18098/) (2026)

## Abstract (arXiv)

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.