An interactive introduction to the Lean theorem prover and “a part-book part-game which shows the power of induction”.
You must log in or # to comment.
I don’t know if it is hosted somewhere, but there’s already a (not completed) Lean4 version: https://github.com/PatrickMassot/NNG4