Lean Tutorial in Lean

Stream: new members

[Rudy Peterson]

Hello,

I am starting to learn Lean, and I am looking for a Software Foundations or PLFA style tutorial. The books Functional Programming in Lean, and Theorem Proving in Lean 4 look super helpful, but is there something where the tutorial itself is given as Lean files or scripts with examples and exercises?

Thanks!

[Daniel Weber]

The Mechanics of Proof has a github repository with code at https://github.com/hrmacbeth/math2001

[suhr]

Типизированная математика is built around examples and exercises. It has a repo with examples and exercises (check out Nat.lean), and the repo of the book contains solutions to the exercises.