This is a really good explanation, but it reinforces my understanding that these “junk maths” are literally undefined behavior as in C and such. They are not defined (in maths), you are not supposed to trigger them, so they can be anything. Great…

This is horrible for a language whose whole purpose I thought was that to be foolproof and that if it compiles its true. Having very subtly different definitions of common operations is such a footgun.

Of course, I understand that this doesn’t bother mathematicians because they are used to not having any guardrails anyways. Just like C programmers have the attitude that if you fall on such a trap, you deserve it and you are not a “real programmer”. But Lean is supposed to be the other extreme isn’t it? Take nothing for granted and verify it from the ground up.

I suppose I am falling for that “Twitter confusion” the post is referring to. I never had any issues with this when actually using Lean. I just don’t like the burden of having to be paranoid about it, I thought Lean had my back and I could use it fairly mechanically by transforming abstract structures without thinking about the underlying semantics too much.

Anyway, despite the annoyance, I do assume that the designers know better and that it is a pragmatic and necessary compromise if it’s such a common pattern. But there must be a better solution, if having the exception makes it uncomfortable to prove, then design the language so that it is comfortable to prove such a thing. Don’t just remove the exception because 99% of the time it doesn’t matter. If we are happy with 99% we wouldn’t be reaching for formal verification, there are much more practical means to check correctness.

I feel like this aged like milk because it assumes a human mathematician writing the proof but many people are now generating Lean proofs with LLMs.

Thank you! This hit the nail on the head for me, though I probably need to try out a few more examples to fully convince myself.

TL;DR: It's actually harmless (and often convenient) to "inflate" the domains of partial functions to make them total (by making them return arbitrary junk values where the original function is undefined), provided that every theorem you want to apply still comes with the original, full restrictions.

Kevin's example is good. My stupider example would be: We can define a set that contains the integers ..., -2, -1, 0, 1, 2, ..., plus the extra element "banana". If we define the result of any addition, subtraction or multiplication involving a banana to be 42, and to have their usual results otherwise, then, provided that we add the condition "None of the variables involved is banana" to the theorem "x+y = y+x", and to every other theorem about arithmetic, anything that we can prove about arithmetic on elements of this set is also true of arithmetic on integers.