I talk about my positive experience trying out the tools for Lean, specifically the 'lean' executable and lean-mode in emacs.