Quine's New Foundations really is consistent!
Randall Holmes announced that he had a proof a while back, and posted various versions. But now the key part has been verified in Lean (by Sky Wilshaw, a Part III student here in Cambridge, building on work done by other students last year).
You can find their paper giving the current best version of the proof here: https://randall-holmes.github.io/Nfproof/maybedetangled2.pdf
As they say in their introduction, the proof goes via a ‘quite bizarre system‘ (so-called tangled type theory) and is 'insanely involved with nasty bookkeeping’? There have been rather more inviting introductions to papers! But still, an insanely intricate and messy but verified-in-Lean proof of consistency relative to a fragment of ZFC still is a consistency proof.
My strong impression is that the general lack of love for NF among set-theorists hasn’t latterly been really grounded in lively doubts about its consistency. So I rather suspect that, even though the proof resolves a very long-standing open problem, its wider impact might well be quite modest. Still, all credit to Randall Holmes for having brought his proof project to a successfully verified outcome.
