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.