Lean is a proof assistant developed mainly by Microsoft Research. It is the first proof assistant that successfully draws attention of mathematicians, particularly, Kevin Buzzard.