Theorem Proving in Lean [pdf]
leanprover.github.io
Theorem Proving in Lean [pdf]
1–10 of 23 posts
Re: Theorem Proving in Lean [pdf]
#2Here's the HTML version of the same thing:
Re: Theorem Proving in Lean [pdf]
#3I'll have to work through this when I get the time.
I started teaching myself Haskell for fun about a year and a half ago, and ended up going down a rabbit hole of formal logic, set theory, mathematical foundations etc. which I did not expect at all; I'm currently spending some time looking at algebraic topology to give me a grounding to go into homotopy type theory.
For anyone else with an interests in this area, I'd strong urge you to look at some of the work from Kevin Buzzard (Imperial College), perhaps better known as an algebraic number theorist, who leads the Xena [1] Project, which started as an attempt to completely formalise all the problem sheets for one of the undergraduate maths modules at Imperial in Lean. There's also a GitHub repo [2] with a lot of work to build on.
Adam Chlipala (MIT) also teaches a course in formal program verification in Coq based on his book [3] which is a valuable resource.
1: https://xenaproject.wordpress.com/
Re: Theorem Proving in Lean [pdf]
#4Why 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?
Re: Theorem Proving in Lean [pdf]
#5Why 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?
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, in your view?
Re: Theorem Proving in Lean [pdf]
#6Why 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?
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/
Also, afaik it won't differ from Lean 3 to the degree where learning Lean 3 is useless.
Re: Theorem Proving in Lean [pdf]
#7I'll have to work through this when I get the time. I started teaching myself Haskell for fun about a year and a half ago, and ended up going down a rabbit hole of formal logic, set theory, mathematical foundations etc. which I did not expect at all; I'm currently spending some time looking at algebraic topology to give me a grounding to go into homotopy type theory. For anyone else with an interests in this area, I'…
So is homotopic type theory just another way to look at the same thing or is it more expressive than type and set theory?
In other words, does homotopic type theory really help theorem checkers/provers?
Re: Theorem Proving in Lean [pdf]
#8I'll have to work through this when I get the time. I started teaching myself Haskell for fun about a year and a half ago, and ended up going down a rabbit hole of formal logic, set theory, mathematical foundations etc. which I did not expect at all; I'm currently spending some time looking at algebraic topology to give me a grounding to go into homotopy type theory. For anyone else with an interests in this area, I'…
So is homotopic type theory just another way to look at the same thing or is it more expressive than type and set theory? In other words, does homotopic type theory really help theorem checkers/provers?
Yes. Also it includes topology.
Re: Theorem Proving in Lean [pdf]
#9I'll have to work through this when I get the time. I started teaching myself Haskell for fun about a year and a half ago, and ended up going down a rabbit hole of formal logic, set theory, mathematical foundations etc. which I did not expect at all; I'm currently spending some time looking at algebraic topology to give me a grounding to go into homotopy type theory. For anyone else with an interests in this area, I'…
So is homotopic type theory just another way to look at the same thing or is it more expressive than type and set theory? In other words, does homotopic type theory really help theorem checkers/provers?
Whether HoTT is a better foundation of mathematics (FOM) in the sense of being easier to use in practise is an open question. It's unclear even exactly what it means to be a better or worse FOM.
Note also that all well-known foundations, including HoTT are mutually relatively consistent, which amounts to being translatable into each other (so if you can derive a contradiction in one, then you can convert that into a contradiction in the other). However that is not so important in practice. Proof automation is most important for large scale reasoning. Indeed the Lean project was started with the explicit aim of bringing better proof automation to provers based on the Curry-Howard correspondence.
Re: Theorem Proving in Lean [pdf]
#10Why 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?
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.