[tux3]

There is still a guardrail. The blog post explains that it is just using different functions and notation which might allow things like 0/0. But at the end of the day, different notation still cannot be used to prove false things.

In other words, you can use all these junk theorems to build strange results on the side, but you can never build something that disagrees with normal math or that contradicts itself. There is no footgun, because the weird results you obtain are just notation. They look weird to a human, but they don't allow you to actually break any rules or to prove 1=0.

[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.