Here 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

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