I've spent another couple of hours playing with Lean, following @XenaProject's Formalising Mathematics course (github.com/ImperialColleg…)
I think the hardest part for me is remembering what each notation really represents, like ¬ P is really (P → false)