https://xenaproject.wordpress.com/2020/07/05/division-by-zero-in-type-theory-a-faq/ https://xenaproject.wordpress.com/2020/07/05/division-by-zer... explains Le

https://xenaproject.wordpress.com/2020/07/05/division-by-zero-in-type-theory-a-faq/ https://xenaproject.wordpress.com/2020/07/05/division-by-zer... explains Lean's behavior. Basically, you use a goofy alternate definition of division (and sqrt, and more), and to compensate you have to assume (or prove based on assumptions) that the things you will divide by are never zero. Hillel's pedantry is ill-taken, though, because he starts off with a false accusation that the headline tweet was insulting anyone. Also, 1/0=0" is sound only if you change the field axiom.of division, which is fine, but quite rather hiding the ball. If you add " 1/0=0" as an axiom to the usual field axioms, you do get an unsound system.