# New Foundations is consistent

We give a self-contained account of a version of the proof of Holmes and Wilshaw
[
4
]
that Quine’s set theory

*New Foundations*[ 5 ] is consistent relative to the metatheory ZFC. This version of the proof is written in a style that is particularly amenable to the formalisation in Lean [ 8 ] ; to that end, type-theoretic concerns and dependencies between parts of the proof are explicitly spelled out.