Questions on proof assistants

[Timothy Y. Chow]

Hendrik Boom wrote:

> On Wed, May 13, 2020 at 08:34:58PM -0400, Timothy Y. Chow wrote:
> ...
>>
>> 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).
>
> We could hope that it wuold be easy to mechanically convert proofs from old
> versions of Lean to new ones.
>
> Are they really *that* incompatible?

Someone who actually knows Lean should answer this question, but for 
example I believe that Lean 2 libraries were *not* in fact converted to 
Lean 3 libraries, so that doesn't bode well.  Also, Kevin Buzzard tells me 
that the entire typeclass system is being rewritten in Lean 4.  This 
sounds to me like a rather fundamental change.  Maybe a mechanical 
conversion of the old libraries would fail to take advantage of the new 
typeclass system and therefore partially defeat the purpose of the 
upgrade?

Kevin Buzzard's response to the question of the interoperability of 
different proof assistants is an interesting one.  When it comes to 
ordinary software, it is routine practice to completely discard old code 
and start afresh.  I remember in the early days of Java, one mantra was 
"write once, run anywhere."  Nowadays, a more accurate mantra for Java is 
"write once, run nowhere" because Java has had so many security holes that 
many browsers disable it by default.  But who cares?  Java is old news. 
There are new programming languages coming out all the time.  If you want 
something, just rewrite it.

Now I think when it comes to formal proofs, most mathematicians 
instinctively balk at this kind of philosophy.  The Flyspeck project 
finished successfully with a formal proof of the Kepler conjecture. 
Suppose I want to use the Kepler conjecture as a step in my own proof. 
Instinctively, it feels wrong to take the attitude, "Well, if you need it, 
just rewrite the proof yourself."  Who is really going to do that?  If one 
day the classification of finite simple groups (CFSG) is formalized, do we 
expect to have to re-implement it every couple of years when there's a 
software upgrade or a hot new proof assistant du jour?  I don't think 
these are "wrong questions" as Buzzard seems to suggest.  We no longer 
have much need for software that reads 5.25" floppy disks, so it's no big 
loss if that software dies.  But we *do* expect to use CFSG for many 
decades if not centuries to come.

It's possible that we have to let go of the "prove once, use forever" 
mentality as a naive youthful dream of formalized mathematics that is just 
not realistic.  Still, if we let go of too many dreams, then we should ask 
ourselves what is left.  For example, driving down error rates is another 
dream that may be unrealistic, as I've discussed on FOM before:

https://cs.nyu.edu/pipermail/fom/2014-August/018067.html

Another dream is that once a proof is formalized, the running time 
requires for a computer to check the proof will be negligible.  This dream 
we already know is likely to be shattered.  Flyspeck is a case in point. 
There are increasingly many theorems whose proofs require thousands of 
hours of computer time even without formalization.  It seems inevitable 
that people are going to want to be able to use such theorems without 
having to check the proof each time, and once that starts to happen, the 
chances of errors creeping in is going to rise.

None of this is to denigrate formal proofs or proof assistants, which I do 
believe are the way of the future.  But it's probably worth getting our 
story straight about what we can realistically expect from them.

Tim