Questions on proof assistants

[Hendrik Boom]

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?

-- hendrik