For me, the best route is to start with Functional Programming in Lean [1]. Get familiar with dependent type theory and Lean's syntax. Then go back to Lean's so

For me, the best route is to start with Functional Programming in Lean [1]. Get familiar with dependent type theory and Lean's syntax. Then go back to Lean's source code [2]. Lean is self-hosted, so the language is written in Lean. And it's well documented. Starting from the Prelude [3], all the way up to the language server (yes, Lean ships a parser combinator library and a JSON library with the language). One caveat is that the toolchain version of the repo is the repo itself, so you'd have to follow the development guide [4] to set it up. Also, this is different from the standard library std4 [5], which is actually not shipped with the language, but just a normal package developed and used as the standard library. [1]: https://leanprover.github.io/functional_programming_in_lean/ https://leanprover.github.io/functional_programming_in_lean/ [2]: https://github.com/leanprover/lean4 https://github.com/leanprover/lean4 [3]: https://github.com/leanprover/lean4/blob/master/src/Init/Prelude.lean https://github.com/leanprover/lean4/blob/master/src/Init/Pre... [4]: https://github.com/leanprover/lean4/blob/master/doc/dev/index.md https://github.com/leanprover/lean4/blob/master/doc/dev/inde... [5]: https://github.com/leanprover/std4 https://github.com/leanprover/std4