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

xenaproject.wordpress.com

Lean is better for proper maths than all the other theorem provers

https://xenaproject.wordpress.com/2020/02/09/lean-is-better-for-proper-maths-than-all-the-other-theorem-provers/

1 comments

ncmncm6 yıl önce

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.