4 ms·
Lean is better for proper maths than all the other theorem provers
- ncmncm 7y agoThe 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.