Questions on proof assistants

[Timothy Y. Chow]

I have had some interesting discussions with Kevin Buzzard about Lean. 
Buzzard is convinced that Lean is the way to go for mathematicians.  One 
of the big selling points is that (he claims) of all the proof assistants, 
it has implemented the largest fraction of the standard undergraduate 
mathematics curriculum.  I do think that this is an important selling 
point, and it is somewhat surprising that the other proof assistants 
haven't accomplished this already.  But there are of course sociological 
reasons behind this.

A couple of years ago, Tom Hales wrote a very interesting review of Lean.

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

I would say that the main reason I haven't dived into Lean is that it 
seems not to have stabilized yet.  Lean version 3 is not compatible with 
Lean version 2, and Lean version 4 (which isn't ready yet) will not be 
compatible with Lean version 3.  Lean version 4 may address some of 
Hales's criticisms but at the cost of breaking many of the existing 
libraries (which, as I said, are one of the best features of Lean).

There is also the problem that there still isn't very good documentation 
that is user-friendly for the average mathematician who is not a skilled 
programmer.  But this criticism is not unique to Lean.  There's a bit of a 
vicious circle here: Mathematicians don't show much interest in proof 
assistants in part because the documentation and user interface are not 
designed with mathematicians in mind, and the documentation is the way it 
is because mathematicians haven't shown much interest.

Tim