I much prefer this resource over the official offerings. https://lean-lang.org/theorem_proving_in_lean4/title_page.html https://lean-lang.org/theorem_proving_i

I much prefer this resource over the official offerings. https://lean-lang.org/theorem_proving_in_lean4/title_page.html https://lean-lang.org/theorem_proving_in_lean4/title_page.ht... You may need to use them in tandem, but I have found it much more productive to jump to the “number theory” section of TFA then to step through the official resource. This resource also has its code online: https://github.com/hrmacbeth/math2001/tree/main/Math2001 https://github.com/hrmacbeth/math2001/tree/main/Math2001 One major ommission from TFA is lean's built in package manager and package builder lake: https://lean-lang.org/lean4/doc/setup.html#lake https://lean-lang.org/lean4/doc/setup.html#lake