The consistency of NF in Lean? - MUCH FUN

[Timothy Y. Chow]

Dennis Hamilton wrote:

> 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."

One thing that bothers me about Lean is that the community has put a lot 
of effort into building libraries for Lean 3, but Lean 4 is incompatible 
with Lean 3.  I suppose people will figure out ways of porting Lean 3 
libraries to Lean 4 without having to re-program everything from scratch, 
but even without knowing anything about the low-level details of Lean, I 
can foresee several problems.

1. There is probably a limit to how much the process can be automated, 
meaning that it will still require a lot of human labor.

2. There is a risk of subtle shifts in meaning during the transition, 
resulting in theorems that don't quite mean what you think they mean.

3. Automatic translation of Lean 3 to Lean 4 may result in some of the key 
features of Lean 4 not being fully exploited, defeating the purpose of the 
upgrade.

One also has to wonder how many times this process of upgrading the 
software and breaking all the libraries will happen in the future.  Three 
more times?  Ten more times?  A hundred more times?  Philosophically, 
mathematicians want a corpus of proved theorems to remain static.  But the 
philosophy of software development seems to be that the higher the version 
number, the better.

Despite these reservations, I do think that Lean is currently the best 
choice for most "working mathematicians" who want to learn a proof 
assistant and is also the best choice for the Conifer project.  The online 
community is very helpful.

Tim