Hey! I heard that Lean thinks 1/0 = 0. Is that true?
Yes. So do Coq and Agda and many other theorem provers.
[...]
But doesn’t that lead to confusion?
It certainly seems to lead to confusion on Twitter. But it doesn’t lead to confusion when doing mathematics in a theorem prover. Mathematicians don’t divide by 0 and hence in practice they never notice the difference between real.div and mathematical division (for which 1/0 is undefined). Indeed, if a mathematician is asking what Lean thinks 1/0 is, one might ask the mathematician why they are even asking, because as we all know, dividing by 0 is not allowed in mathematics, and hence this cannot be relevant to their work.
Schlagwort: Mathematik
Leanorris.
Nice but late.
“But there is no honor in elegantly proving a theorem in 1672 that some Scotsman proved barbarously in 1671!”
Neal Stephenson: Quicksilver
No arrows, not even objects.
Am I the only one who annoyed by "functor" in Prolog?
Teilen mit Rest.
Bistromathics itself is simply a revolutionary new way of understanding the behaviour of numbers.
Douglas Adams: The Restaurant at the End of the Universe
☡.
The dangerous bend or caution symbol ☡ [...] was created by the Nicolas Bourbaki group of mathematicians and appears in the margins of mathematics books written by the group. It resembles a road sign that indicates a "dangerous bend" in the road ahead, and is used to mark passages tricky on a first reading or with an especially difficult argument.