Content
@
0 reply
0 recast
0 reaction
Agost Biro
@agostbiro
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
1 reply
0 recast
8 reactions
cqb
@cqb
Will you make a pr with useful things that you think would make the book more approachable?
1 reply
0 recast
0 reaction
Agost Biro
@agostbiro
Possibly once I've finished it, but I don't feel experienced enough yet to propose changes
1 reply
0 recast
1 reaction
cqb
@cqb
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
1 reply
0 recast
1 reaction
Agost Biro
@agostbiro
Yeah, def these posts will be helpful to provide feedback
0 reply
0 recast
1 reaction
