The same JavaScript code compiles to different machine representations under different browser engines; yet webdevelopers don't need to learn assembly.

There is an abstract javascript machine which can obviously be translated to hardware instructions. "Obvious" in the mathematical research sense, as in the statement is flat out wrong under closer inspection. Websites regularly crash under memory pressure.

But they are good enough most of the time, and that's the key. With more resource a more correct program can be created, but cost-benefit calculations show a ceiling. A local pet store does not have the money to pay 2000 hours of formal verification work, and usually a WordPress site is good enough.

Mathematicians work with their brains. They have finite time to understand papers. Formalists say that all theorems could be reduced to logical axioms, but most of time it's jumping at a much higher level, because no one has time for minute details. Proofs are theoretically right or wrong, but in practice there are "slightly wrong" proofs, where there are some minute errors that "feels" like can be correcte, and most of the time it can be. This ambiguity is not a problem, but a feature of mathematics, because it means more time can be spent to move faster at a higher level of abstraction, but this would be lost with Lean.

Is not a natural language (NL) proof a demonstration of mastery and understanding?

If you understand the Lean, then you can create a NL proof. The LLM clearly doesn't understand the Lean code it produced.