3 ms·
> But you allow seemingly nonsense theorems when you forget to condition (x>0). Such as what? I’ve only spent a few hours with lean, but I’m fairly sure that a
by empath75 6y ago
> But you allow seemingly nonsense theorems when you forget to condition (x>0).
Such as what? I’ve only spent a few hours with lean, but I’m fairly sure that any attempt to prove something silly would fail because it would catch the weird behavior of 0.
For example. If you tried to use a/a = 1 as the article mentions, you’d be unable to prove it without adding the condition that a != 0, and you’d be unable to use it further on without that condition in place.
- leanuser57 6y agoHere is a "nonsense" theorem that is provable in Lean: “There exists a real number r such that 1/r = 0.” If you try to translate this theorem into maths, you will run into trouble at some point. At which point exactly depends on how you want to make things precise... which is exactly what mathematicians avoid when talking about division in fields.
- empath75 6y agoThat’s a perfectly sensible function, it’s just not ordinary division on the reals where x = 0, and you can’t use it that way.