4 ms·

I would assume he chose Lean because it is what Kevin Buzzard has popularized and has been used to prove some very complex theories.