In this episode, I talk about what I have learned so far about the Lean prover, especially from an excellent (if somewhat advanced) Master's thesis, "The Type Theory of Lean" by Marco Garneiro.