Lean is better for proper maths than all the other theorem provers (xenaproject.wordpress.com)

The article uses the wonderful "WLOG" acronym, short for WLOTAIG, which is in turn short for "Without Loss of That All-Important Generality".

Piling on, I wouldn't mind seeing a formalization of Grigori Perelman's proof of the Poincaré conjecture. But I am probably dreaming.