Lean is particularly exciting because of the work Kevin Buzzard has been doing in the Xena project: https://www.ma.imperial.ac.uk/~buzzard/xena/ https://www.ma

Lean is particularly exciting because of the work Kevin Buzzard has been doing in the Xena project: https://www.ma.imperial.ac.uk/~buzzard/xena/ https://www.ma.imperial.ac.uk/~buzzard/xena/ He started by getting undergraduates to tackle formalising the maths they did in Lean, and his success with this as a didactic tool has spread the idea among quite a lot if mathematicians.