learnlean

So I've been following the Mathematics in Lean book which I mostly like, but the exercises are not well designed. To solve the pictured exercise,[1] it gives you a bunch of theorems to use, plus you're supposed to remember a magic incantation (`linarith`) from the previous chapter to solve it. But `linarith` isn't really well explained there, nor is there an exercise to practice its usage.

Removing the hand-wavy magic from math is exactly why I started learning Lean, so instead of taking these as given, I rabbit-holed on how `linarith` and `abs_nonneg` work and added my findings as comments. 

And this shows the power of Lean. Just by using jump to source and a bit of Googling, I was able to get a good understanding of how these things work. If this exercise was in a text book presented like this, I probably wouldn't have gotten there.

[1]

So I've been following the Mathematics in Lean book which I mostly like, but the exercises are not well designed. To solve the pictured exercise,[1] it gives you a bunch of theorems to use, plus you're supposed to remember a magic incantation (`linarith`) from the previous chapter to solve it. But `linarith` isn't really well explained there, nor is there an exercise to practice its usage.

Removing the hand-wavy magic from math is exactly why I started learning Lean, so instead of taking these as given, I rabbit-holed on how `linarith` and `abs_nonneg` work and added my findings as comments. 

And this shows the power of Lean. Just by using jump to source and a bit of Googling, I was able to get a good understanding of how these things work. If this exercise was in a text book presented like this, I probably wouldn't have gotten there.

[1] https://leanprover-community.github.io/mathematics_in_lean/C02_Basics.html

OSS + Rust. I have one goal in life: the ability to stop thinking at will

Will you make a pr with useful things that you think would make the book more approachable?

Interested in ZK, FHE, PUFs, hardware, system design, ai safety, and smart contact security.

It might be helpful to just open an issue for any of the pain points you've had, that way there are some pointers to places that need improvement even if you don't feel qualified to propose changes

Possibly once I've finished it, but I don't feel experienced enough yet to propose changes