The consistency of NF in Lean?

[JOSEPH SHIPMAN]

Remind me, what’s the consistency strength that was claimed?

Sent from my iPhone

> On Feb 27, 2022, at 12:16 AM, Timothy Y. Chow <tchow at math.princeton.edu> wrote:
> 
> 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