Very nice to see you here Kevin. We never interacted but I do still remember a l...

		mherrmann on June 19, 2021 \| parent \| context \| favorite \| on: Mathematicians welcome computer-assisted proof in ... Very nice to see you here Kevin. We never interacted but I do still remember a lecture you gave at Imperial in '06 where you filled in for Prof. Liebeck and started with Lemma 1: "I am not Professor Liebeck" ;-) Thank you for the nice memory and your important work on / with Lean.

Did he prove the lemma or did he leave it as an exercise :-) ?