kevinzz

Lean 4 is no longer being developed in private; this was true a year ago but is no longer true. What is true is that Lean 4 is still not ready for the port of the maths library to begin, and we do not know when it will be. Furthermore, one cannot yet use Lean 4 within VS Code, which makes it more inconvenient to use than Lean 3. But we can wait. Lean 3 is good enough to do a lot of modern mathematics so it seems, and the community are happy to work with Lean 3 currently.

There is every way of knowing how much will be obsolete in Lean 4, as long as you're following the discussions at https://leanprover.zulipchat.com . The type theory of Lean 4 will be the same as Lean 3, there are some minor syntax changes and conventions for variable naming have changed from this_way to ThatWay but all the type theory is the same and the book will be an excellent introduction to Lean 4.

The main issue with Lean 4 is that there is currently no tactic state, but the designer Leo de Moura is currently hard at work at this, because they need tactics to start work on their IMO Grand Challenge https://imo-grand-challenge.github.io/ . Even when tactics are done, there will be no type class inference so the port of the maths library from Lean 3 to Lean 4 will probably not begin then. Type class inference is a complex issue and some of the chat on the zulip chat is about issues that users have been having in Lean 3 and how they might be fixed in Lean 4. But, in short, the basic principles are all the same. In short, I would thoroughly recommend this book.

The headline is clickbait. A more measured debate about the issues is here https://xenaproject.wordpress.com/2019/09/27/does-anyone-kno...

In Lean you could do

  theorem and_commutative (p q : Prop) : p ∧ q → q ∧ p := by cc

for a tactic proof and

  theorem and_commutative (p q : Prop) : p ∧ q → q ∧ p := λ ⟨h,j⟩,⟨j,h⟩

for a term proof (just write down the function).