5
$\begingroup$

Porting Mathlib from Lean 3 to Lean 4 is a huge effort, and I'm sure it's not undertaken on a whim. Could you please point me to documentation explaining the motivation for the incompatible changes? Is Lean 4 faster? More expressive?

The Lean 4 survival guide for Lean 3 users showcases many changes, but those look superficial to me.

$\endgroup$
4
  • 1
    $\begingroup$ Sorry for the basic question. Google search results are all fitness motivation videos and discussion of goals in the theorem proving sense. :( $\endgroup$ Jun 9, 2023 at 12:12
  • $\begingroup$ Perhaps "leanprover" is a good search keyword. That's the downside of naming your language with a common word! $\endgroup$
    – Trebor
    Jun 9, 2023 at 13:19
  • 2
    $\begingroup$ It looks like the port will be finished in a few weeks, by the way; the community is over 80% of the way through. $\endgroup$ Jun 9, 2023 at 15:48
  • $\begingroup$ I saw! I wrote 71% in a doc a week or so ago and today it's 85%! Fantastic work! That's why I want to know exact what I'm excited for! :) $\endgroup$ Jun 9, 2023 at 17:50

1 Answer 1

8
$\begingroup$

There are many aspects to this:

  • It's faster (e.g. the ~80% portion of mathlib that has been ported so far compiles between 3 and 4 times faster than it did under Lean 3.)
  • The metaprogramming framework (which is even more different relative to Lean 3 than the proving experience) is massively more capable. Most of Lean 4 is written in Lean 4, and users adding tactics can hook into and modify the internals in all sorts of new ways.
  • It's intended as a general purpose programming language, not just an interactive theorem prover. (Lean 4 produces quite impressively fast executables. You can call into C++. It has reference counting tricks that allows functional code to be compiled to update-in-place when appropriate, and the Do unchained paper explains how to write functional code in an imperative style.)
  • The type theory itself is essentially unchanged, although there are some usability improvements (in particular typeclass search is faster, and can cope with loops).
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.