[FOM] Improving Set Theory/Self Proving

[Timothy Y. Chow]

On Mon, 13 Jan 2020, Harvey Friedman wrote:
> I was referring more to sociological/practical issues. I was reading 
> this from a source who is a working expert in Proof Assistance. I just 
> can't recall the reference.
>
> The idea I read is that "it is virtually impossible to get funding 
> agencies to see enuf need to grant the required resources to get, say, 
> FLT formally verified with the best arguments for what is to be gained 
> by doing so".

Okay, I've heard this too, and personally I don't need to see an explicit 
reference or detailed discussion of this point.  I believe it.

On the other hand, I am interested in what obstacles are preventing proof 
assistants from becoming as widely adopted as, say, computer algebra 
systems or even LaTeX.  Buzzard's enthusiasm for Lean, and his mention of 
Tom Hales, led me to discover the following very interesting blog post by 
Hales:

https://jiggerwit.wordpress.com/2018/09/18/a-review-of-the-lean-theorem-prover/

The bottom line is that Hales likes Lean better than the alternatives, but 
he also articulates a number of searching criticisms of it.  The blog post 
was written in September 2018, and of course there have been several 
developments since then, but many of Hales's remarks are still relevant. 
Notably, Lean is still not stable---Lean 4 is the current version, and it 
indeed breaks many of the old libraries---and the learning curve is very 
steep because the documentation is poor.  Of Hales's criticisms, the one 
that will probably be most startling to mathematicians---that there is a 
fundamental distinction in Lean between groups that use the symbol * for 
the group operation and groups that use the symbol + for the group 
operation---is still true.

In short, there still seems to be room for fresh design ideas.  Of course 
there remains the problem that ideas are cheap, while writing a kernel and 
building libraries and creating documentation and building a user base are 
expensive.

Tim