Randall Holmes has been claiming a proof for about a decade, and recently posted yet another improved update of his proof on arXiv.
A while back, there was some very interesting discussion about the possibility of formalising the proof using a proof assistant like Lean. There’s now some relevant local news, which I get from Thomas Forster.
Roughly speaking, the proof has three components. (1) Randall proved over twenty-five years ago that NF is consistent if what he called Tangled Type Theory, TTT, is. Arm waving, if a sentence 
is a correctly typed sentence of the simple theory of types, and 
is what you get by replacing the type levels in with new type levels with the same order relation, then is a sentence of TTT. So where in the simple theory, for 
to be well formed, 
has to be one type higher than 
, in TTT is well-formed even when is more than one type higher than , so there is an 
relation between any lower level and any higher level. This relative consistency claim of NF and TTT is unproblematic.
(2) TTT is a seemingly rather wild theory (Holmes calls it “weird”). But Holmes now aims to present a Frankel-Mostowski-style construction that purports to be a model of TTT. The devil is in the contorted(?) detail: do we get a coherent description of a determinate structure?
(3) Assuming that stage (2) is successful in at least describing a kosher structure that a ZF-iste can happily accept as such, there then is the task of verifying that it really is a model of TTT.
Now, over the last few weeks, a bunch of maths students here have been working on a summer project arranged by Thomas (with a lot of Zoomed input from Randall) to formally verify the consistency proof in Lean, by first checking (2) that the model is coherently constructed, and then going on to check (3) it really is a model of TTT. And I understand the state of play to be this: that first of these stages is successfully more or less completed. And it has in the process become intuitively clear — said Thomas — that the defined structure is indeed a model of TTT. Dotting the i’s and crossing the t’s and implementing a Lean check that the model satisfies a certain finite axiomatization of TTT will take more time than there is left in this summer’s project (the students have lives to lead!). But with (2) secure, it looks as if Holmes indeed has his claimed proof, though its final best-form shape remains to be settled.
If that’s right, Holmes has settled one of the oldest open problems in set theory. Though quite what the wider significance of this, I’m frankly not so sure. Will a consistency proof (of a decidedly tricksy-seeming kind) really make us look much more kindly on NF? Should it?
What is ‘wild’ (or even ‘Tangled’) about TTT? It looks like a fairly simple generalisation, though looks can, of course, be deceiving.
(BTW, the “Arm waving” sentence is missing a “get” in “is what you from” and a “than” in “one type higher x“.)
Maybe I underdescribed and made TTT seem tamer than it is. Cf. Randall’s papers, and also https://mathoverflow.net/questions/427351/can-we-write-tangled-type-theory-without-reference-to-type-sequences
The idea that stratification is just a syntactic trick has been around for a long time, and the time has come to pursue the possibilities to be found on the other horn.
I’m not sure that Dana would say that now! There is a growing appreciation (arising at least in part from work done by him) that stratification is more than just a syntactic trick, and has some genuine mathematical significance. Confirmation of Randall’s result will spread that appreciation further. It certainly should! We shall see….
Sorry I should have given more context to the quote, however in the end I do think he would still agree with it.
The quote is from his “A type-theoretical alternative to ISWIM, CUCHY, and OWHY” paper, which was written before his work in finding models for untyped lamba calculi (and therefore is hostile to the idea of untyped formal systems, of which he explicitly does not count ZF), but was published decades after. However, there is a footnote (added during the publication process) at the end of the exact sentence I quoted which reads “The author still believes this statement.” Granted, that footnote was written in 1993, but I do think there is a good chance he would still believe it today as well given why he still believed it then.
I’ve been periodically looking at the progress of this project and I think it’s very interesting in a historical sense that this specific problem ended up being solved (or, at least, the solution being verified) with the help of a proof assistant.
In terms of what it means for how people view NF, I am inclined to agree still with this quote by Dana Scott, “Russell (with the help of Ramsey) had the right idea, and Curry and Quine are very lucky that their unmotivated formalistic systems are not inconsistent.”