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.
“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.
Or assume it. This is what you have to do in real life anyway. If you can't assume the inputs are nonzero you have to prove it. Otherwise the proof doesn't work.
1. The article's way: "R^2->R", but garbage value for 0 in the second argument.
2. What you propose: "R^2->Maybe R"
3. The mathematician's dependent-type-theoretic way "R * (x:R, proof that x!=0) -> R",
4. the conventional way "R * (R\{0}) -> R".
They have their advantages and disadvantages. The first is useful in proof verification since it simplifies most proofs, from which perspective this garbage value of 0 is actually well-behaved, and doesn't need to be handled as a special case. But you allow seemingly nonsense theorems when you forget to condition (x>0).
What you propose is similar, except that you are forced to reason about whether the output value is valid.
3 and 4 are tedious, since you always need to prove that the inputs are nonzero. 4 is more tedious since you have merely shifted the problem of handling the zero case into proving properties about the canonical embedding "R->R\{0}" (which must still have a garbage value for 0). On the upside, these functions surject into R.