Disclaimer: I’ve started reading the Lean guide for the past month or two.
For me the most magical texts I have ever read were TAPL by Pierce, or the Lean Theorem Prover (tutorial/guide?) [1].
Just from a software standpoint, Lean seems like one of the most magical things ever built. For something that is built by mathematically-oriented programmers for pure mathematicians, it is /extremely/ well designed. So much thought has seemed to go into the user experience; it’s rest a joy to use.
Every chapter in that guide, has blown my mind more than the previous. It is super accessible as well to anyone with the math background found in any undergrad CS program.
For me the most magical texts I have ever read were TAPL by Pierce, or the Lean Theorem Prover (tutorial/guide?) [1].
Just from a software standpoint, Lean seems like one of the most magical things ever built. For something that is built by mathematically-oriented programmers for pure mathematicians, it is /extremely/ well designed. So much thought has seemed to go into the user experience; it’s rest a joy to use.
Every chapter in that guide, has blown my mind more than the previous. It is super accessible as well to anyone with the math background found in any undergrad CS program.
[1]: https://leanprover.github.io/theorem_proving_in_lean/introdu...