5 ms·

Lean Book: The Hitchhiker's Guide to Logical Verification [pdf]

177 points by kevinbuzzard 7y ago

enricozb 7y ago
Awesome. I've been looking for more Lean resources outside of Theorem Proving in Lean [1]. [1]: https://leanprover.github.io/theorem_proving_in_lean/ https://leanprover.github.io/theorem_proving_in_lean/
- ahelwer 7y ago
  My favorite is the Natural Number Game: https://wwwf.imperial.ac.uk/~buzzard/xena/natural_number_game/ https://wwwf.imperial.ac.uk/~buzzard/xena/natural_number_gam... A series of levels where you prove ever-more-complex theorems in Lean, gaining each proved theorem as a tool to use in proving further theorems! Best puzzle game I've played in years.
kevinbuzzard 7y ago
Contains a section on the rational and real numbers. Mathematicians might want to start at section 11.5.
- ivanbakel 7y ago
  Since I know you're targeting undergrads with Xena - do you feel that changes are happening in more entrenched academia? Is there any evidence of people using automatic provers who weren't before?
  - kevinbuzzard 7y ago
    There is a huge amount of evidence of mathematics undergraduates using interactive provers, which they weren't doing before. There are very few profs using any interactive prover, because currently these things offer nothing useful to a prof. However, if more and more undergraduates adopt software like this, or at least try it and realise that it's not scary, then within ten years there will be profs using it. We're playing the long game. We need to make tools for the profs, like automation that can check tedious lemmas, or a database of theorem statements which is searchable by a mathematician who doesn't know how to use the software. These are some of the goals Tom Hales is targetting with his FABSTRACTS project. But it will take time. All I know is that the software is now ready to do modern mathematics.
    - ncmncm 7y ago
      In time, the profs will retire, and undergraduates will become profs. Those will expect proofs to have been checked before submission. Mathematics might fission into two fields, one with proofs that cannot practically be formally checked, ultimately akin to philosophy, and rigorous maths that will demand finite checks. Moving results from the former to the latter will occupy some. Exploring whether, and under what conditions, that is possible, for any given result, will have its own interest.
dang 7y ago
Recent and related: https://news.ycombinator.com/item?id=22789953 https://news.ycombinator.com/item?id=22789953 https://news.ycombinator.com/item?id=22390486 https://news.ycombinator.com/item?id=22390486 https://news.ycombinator.com/item?id=21200721 https://news.ycombinator.com/item?id=21200721 https://news.ycombinator.com/item?id=20909404 https://news.ycombinator.com/item?id=20909404 (These are links for the curious. I add that because readers sometimes assume that we're chiding people for posting related things. Pas du tout!)
outlace 7y ago
For those on the fence about learning Lean or some other theorem prover: I highly recommend it if you want to self-learn math. Learning math from a textbook is rather dry and often doesn’t come with solutions. Lean essentially gamifies learning math and you always know if you got the right answer. Moreover, unlike written math which is rife with ambiguous notation (unless you’re an expert), math in a theorem prover like Lean is always unambiguous.
- reuben364 7y ago
  I'm learning lean with that intent (to self learn mathematics). I get distracted trying to learn how to do better proof automation and tactic golf. Also, since I don't see anyone mentioning so it far: there is a currently fairly active Zulip chat for the lean prover. They have been quite helpful for me getting started.
- solomonb 7y ago
  I'm planning to learn Agda for this very reason. Have you looked at Agda or other proof checkers? What about Lean made you decide to use it for this project? The Tactics system?
  - outlace 7y ago
    Yes I've played with Agda before Lean. I found documentation for Agda to be sparse, maybe it's improved since then. Also, it was kind of a pain to get it setup. Lean was extremely easy to get running, works beautifully with VSCode, has great documentation and a helpful community. It's a "sexy" language and set of tooling compared to Agda and Coq (and I'm of the opinion aesthetics matter). It also feels more well-supported with the backing of Microsoft Research behind it.
- ampdepolymerase 7y ago
  You are not really learning how to make proofs though, you are learning how to make specifications. There is an important difference. It is one thing to "prove by induction that this loop will end" and another completely to write a specification for the compiler to find a proof for you. It comes down to the fundamental concept of computability. You won't learn true proving if you don't at least attempt to work through e.g. Cantor or Epsilon-Deltas.
TheUndead96 7y ago
I have bounced off Lean a few times. What I wish I was able to achieve with it was to derive new and useful conclusions in mathematics. I can never seem to get past the "variable is an integer" examples. I realise that the objective in using these tools is exactly the problem in formulating your expression. I think it would be awesome if tools could generate novel mathematics. Where we could express "P=NP" and have computers just churn on that for a few thousand CPU hours.
- zozbot234 7y ago
  > What I wish I was able to achieve with it was to derive new and useful conclusions in mathematics. That's a very high bar, and not likely to be reachable for quite some time. The most worthwhile, reasonably short-term goal in formalized mathematics is "simply" to completely formalize some sizeable part of the undergrad curriculum. (One should note that a proof formalization is publishable work on its own, because the process of formalizing a proof in some given system does help clarify the underlying working of it in a way that's not obvious from an informal sketch.)

177 points by kevinbuzzard 7y ago

Awesome. I've been looking for more Lean resources outside of Theorem Proving in Lean [1]. [1]: https://leanprover.github.io/theorem_proving_in_lean/ https://leanprover.github.io/theorem_proving_in_lean/

ahelwer 7y ago
My favorite is the Natural Number Game: https://wwwf.imperial.ac.uk/~buzzard/xena/natural_number_game/ https://wwwf.imperial.ac.uk/~buzzard/xena/natural_number_gam... A series of levels where you prove ever-more-complex theorems in Lean, gaining each proved theorem as a tool to use in proving further theorems! Best puzzle game I've played in years.

kevinbuzzard 7y ago

Contains a section on the rational and real numbers. Mathematicians might want to start at section 11.5.

ivanbakel 7y ago
Since I know you're targeting undergrads with Xena - do you feel that changes are happening in more entrenched academia? Is there any evidence of people using automatic provers who weren't before?
- kevinbuzzard 7y ago
  There is a huge amount of evidence of mathematics undergraduates using interactive provers, which they weren't doing before. There are very few profs using any interactive prover, because currently these things offer nothing useful to a prof. However, if more and more undergraduates adopt software like this, or at least try it and realise that it's not scary, then within ten years there will be profs using it. We're playing the long game. We need to make tools for the profs, like automation that can check tedious lemmas, or a database of theorem statements which is searchable by a mathematician who doesn't know how to use the software. These are some of the goals Tom Hales is targetting with his FABSTRACTS project. But it will take time. All I know is that the software is now ready to do modern mathematics.
  - ncmncm 7y ago
    In time, the profs will retire, and undergraduates will become profs. Those will expect proofs to have been checked before submission. Mathematics might fission into two fields, one with proofs that cannot practically be formally checked, ultimately akin to philosophy, and rigorous maths that will demand finite checks. Moving results from the former to the latter will occupy some. Exploring whether, and under what conditions, that is possible, for any given result, will have its own interest.

dang 7y ago

Recent and related: https://news.ycombinator.com/item?id=22789953 https://news.ycombinator.com/item?id=22789953 https://news.ycombinator.com/item?id=22390486 https://news.ycombinator.com/item?id=22390486 https://news.ycombinator.com/item?id=21200721 https://news.ycombinator.com/item?id=21200721 https://news.ycombinator.com/item?id=20909404 https://news.ycombinator.com/item?id=20909404 (These are links for the curious. I add that because readers sometimes assume that we're chiding people for posting related things. Pas du tout!)

outlace 7y ago

For those on the fence about learning Lean or some other theorem prover: I highly recommend it if you want to self-learn math. Learning math from a textbook is rather dry and often doesn’t come with solutions. Lean essentially gamifies learning math and you always know if you got the right answer. Moreover, unlike written math which is rife with ambiguous notation (unless you’re an expert), math in a theorem prover like Lean is always unambiguous.

reuben364 7y ago
I'm learning lean with that intent (to self learn mathematics). I get distracted trying to learn how to do better proof automation and tactic golf. Also, since I don't see anyone mentioning so it far: there is a currently fairly active Zulip chat for the lean prover. They have been quite helpful for me getting started.
solomonb 7y ago
I'm planning to learn Agda for this very reason. Have you looked at Agda or other proof checkers? What about Lean made you decide to use it for this project? The Tactics system?
- outlace 7y ago
  Yes I've played with Agda before Lean. I found documentation for Agda to be sparse, maybe it's improved since then. Also, it was kind of a pain to get it setup. Lean was extremely easy to get running, works beautifully with VSCode, has great documentation and a helpful community. It's a "sexy" language and set of tooling compared to Agda and Coq (and I'm of the opinion aesthetics matter). It also feels more well-supported with the backing of Microsoft Research behind it.
ampdepolymerase 7y ago
You are not really learning how to make proofs though, you are learning how to make specifications. There is an important difference. It is one thing to "prove by induction that this loop will end" and another completely to write a specification for the compiler to find a proof for you. It comes down to the fundamental concept of computability. You won't learn true proving if you don't at least attempt to work through e.g. Cantor or Epsilon-Deltas.

TheUndead96 7y ago

I have bounced off Lean a few times. What I wish I was able to achieve with it was to derive new and useful conclusions in mathematics. I can never seem to get past the "variable is an integer" examples. I realise that the objective in using these tools is exactly the problem in formulating your expression. I think it would be awesome if tools could generate novel mathematics. Where we could express "P=NP" and have computers just churn on that for a few thousand CPU hours.

zozbot234 7y ago
> What I wish I was able to achieve with it was to derive new and useful conclusions in mathematics. That's a very high bar, and not likely to be reachable for quite some time. The most worthwhile, reasonably short-term goal in formalized mathematics is "simply" to completely formalize some sizeable part of the undergrad curriculum. (One should note that a proof formalization is publishable work on its own, because the process of formalizing a proof in some given system does help clarify the underlying working of it in a way that's not obvious from an informal sketch.)