The consistency of NF in Lean?

[Timothy Y. Chow]

FOM readers may be interested to know that I asked Randall Holmes about 
the prospects for formalizing his proof of the consistency of NF using the 
proof assistant Lean, in order to address lingering doubts about the 
correctness of the proof.  Holmes responded by saying that he had just 
been thinking the same thing himself.  Some preliminary discussions have 
begun on the online Lean forum.  If you already have a Zulip account then 
you can find the discussion in the #maths stream in the topic on "The 
consistency of NF".  Otherwise, you can view the discussion so far here:

https://leanprover-community.github.io/archive/stream/116395-maths/topic/The.20consistency.20of.20NF.html

Whether this project will come to fruition remains to be seen, but the 
preliminary indications are promising.  Holmes has indicated that he is 
willing to take the lead on the project, subject to the constraints 
imposed by his other commitments.  Mario Carneiro has already taken a huge 
step by attempting to formalize the statement of Holmes's main theory 
(although Carneiro has made it clear that he can devote only a limited 
amount of time to this project going forward).  Thomas Forster has also 
indicated that he would like to help, not by directly working in Lean, but 
for example by supervising interested students.

Forster, by the way, has said that he understands the general structure of 
the proof and believes that it is probably correct, but that because the 
details are so complicated, and have never been fully nailed down in 
writing, he cannot personally vouch for its correctness.  So there do 
remain some legitimate doubts.  I am hoping that this project (which I 
have suggested be called "Conifer" since it sounds a bit like Con(NF)) 
will settle the matter one way or the other.

Tim