Natural language is ambiguous, but the Lean formalization is very well defined and unambiguous.

It's not the form language that is the real problem here. It's the ambiguity on the other side and the extreme difficulty of doing a useful and accurate translation.