I did my undergrad at Imperial. My first lecture was supposed to be with Prof. Liebeck. Kevin came in and wrote on the blackboard: "Lemma 1 - I am not professor Liebeck". He was wearing his (I think typical) trousers. I never interacted with him personally but I did look at his Wikipedia page once. He was the top student in his undergraduate class (Mathematics) at Cambridge. Very impressive to a mere mortal like me.

I once played with Lean but found the tutorial not very approachable. It took an hour of reading through abstract explanations until it finally explained the idea how it works. Essentially, true statements are expressions that pass the "type check" of a compiler. A function taking type A as param and returning type B is an implication A->B. To prove this implication, you need to find a function implementation that passes the corresponding type checks. This is what I would have wanted the tutorial to say at the start.