The consistency of NF in Lean? - MUCH FUN

[dennis.hamilton at acm.org]

That discussion thread is wonderful to read.  Not that I am competent to
participate.

It did renew my interest in Lean, and I'm now curious about having Lean 4
build properly as a Windows PC app.  I have some timidity about that, after
finding the attempt to memorialize Interlisp as completely inscrutable; that
requires tacit knowledge that is only held by those who were on the original
project in the 1970s-80s.  Still, Lean appears to be nice work and I should
probably learn to use it and move helping build it to "someday."

Great discussion.  Thanks for pointing it out.

 - Dennis

-----Original Message-----
From: FOM <fom-bounces at cs.nyu.edu> On Behalf Of Timothy Y. Chow
Sent: Monday, February 21, 2022 09:35
To: fom at cs.nyu.edu
Subject: The consistency of NF in Lean?

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