Comment by crystal_revenge

A lot of people recommend the Natural Number Game for learning Lean, but, as an experienced functional programmer, I don't like it when the code is abstracted away from me. This is not a critique of the tutorial, which is fantastic for it's audience (presumably people more interested in theorem proving without a background in programming), but it might not be ideal for people who want to really get the feel of working in Lean.

For experienced programmers who prefer to learn in the IDE, I've found Theorem Proving in Lean 4 [0] to be a wonderful introduction to an incredible language and area of research. Lean 4 has really nice tooling if you use the VS Code plugin.

Functional Programming in Lean [1] also looks great, but doesn't seem to focus as heavily on understanding theorem proving, which, for me, is the entire point of learning Lean.

0. https://leanprover.github.io/theorem_proving_in_lean4/

1. https://lean-lang.org/functional_programming_in_lean/