3 ms·

Why learn Lean as written in the book when there is no way of knowing how much of it will be obsolete in Lean 4, which is being developed in private?

jbapple 7y ago
Where can I read more about the decision to develop Lean 4 in private, and what is the status of https://github.com/leanprover/lean4 https://github.com/leanprover/lean4, in your view?
- kevinzz 7y ago
  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.
  - mafribe 7y ago
    How would you compare the state of proof automation to be expected from Lean 4 in comparison with Isabelle/HOL? I'm quite familiar with the latter.
foooobar 7y ago
Because the book is a great introduction to theorem proving in general. All those concepts learned translate nicely to other theorem provers, and especially Lean 4. Lean 4 has already gone public: https://github.com/leanprover/lean4/ https://github.com/leanprover/lean4/ Also, afaik it won't differ from Lean 3 to the degree where learning Lean 3 is useless.
kevinzz 7y ago
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 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/ 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.

jbapple 7y ago

Where can I read more about the decision to develop Lean 4 in private, and what is the status of https://github.com/leanprover/lean4 https://github.com/leanprover/lean4, in your view?

kevinzz 7y ago
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.
- mafribe 7y ago
  How would you compare the state of proof automation to be expected from Lean 4 in comparison with Isabelle/HOL? I'm quite familiar with the latter.

foooobar 7y ago

Because the book is a great introduction to theorem proving in general. All those concepts learned translate nicely to other theorem provers, and especially Lean 4. Lean 4 has already gone public: https://github.com/leanprover/lean4/ https://github.com/leanprover/lean4/ Also, afaik it won't differ from Lean 3 to the degree where learning Lean 3 is useless.

kevinzz 7y ago

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 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/ 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.