Terrence talks a lot about his experiences with Lean and the field more generally on his Mastodon over at @tao@mathstodon.xyz