1. 7
  1. 3

    I had been going through the Lean documentation and was basically unable to understand the tactics-based proving flow… and this video is what made it click.

    I still have a hard time really understanding if something like Lean has a place in my life, but it’s been the language I’ve gotten the furthest in thanks to some online videos I’ve found of people walking through non-trivial examples.

    1. 1

      David Christiansen, one of the authors of The Little Typer, is currently writing a textbook called Functional Programming in Lean: https://leanprover.github.io/functional_programming_in_lean/ (also, reading The Little Typer definitely improved my understanding of Lean).

      I haven’t read Functional Programming in Lean yet but it’s in my list for 2023. I hope Lean will be a long term hobby for me, contributing theorems to mathlib.

    2. 2

      I tried using Lean a few years ago to formalize an Analysis textbook. I enjoyed it but the language was changing too fast for me to keep up, so I switched to Coq. I’d like to revisit it sometime if it’s stabilized.