2 ms·
One of my major concerns with Lean 4 is when I asked about mathlib compatibility some 2-3 years ago and the only reply I got was from Kevin Buzzard, implying th
by koito17 3y ago
One of my major concerns with Lean 4 is when I asked about mathlib compatibility some 2-3 years ago and the only reply I got was from Kevin Buzzard, implying that the best we can do is essentially rewrite it all!
Correct me if I am wrong, but I think mathlib still uses a community-maintained fork of Lean 3. I love Lean and its relative ease-of-use compared to e.g. Coq, but man, having to rewrite all of mathlib is a real bummer if that is indeed what has to happen for Lean 4 compatibility.
- mauricioc 3y agoMathlib was fully ported to Lean 4 (https://github.com/leanprover-community/mathlib4 https://github.com/leanprover-community/mathlib4), and the Lean 3 version is deprecated now. Edit: Adding a little bit more detail, it was ported one file at a time, using the automated translation from mathport (https://github.com/leanprover-community/mathport https://github.com/leanprover-community/mathport) as a starting point.