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.