[oersted]

I understand that, but if "/", and other common operators, don't mean what they means on paper, you can prove things that would be untrue if copied onto paper (kinda). You can indeed prove "1/0 = 0", which is not that far off from redefining "=" and proving "1=0".

More importantly, the other way around, it seems too easy to copy a proposition from paper onto Lean and falsely prove it without realising they don't express the same thing. A human probably wouldn't but there's increased usage of AI and other automatic methods with Lean.

I do understand I'm being purist and that it doesn't matter that much in practice. I've used Lean seriously for a while and I've never encountered any of this.