I feel like even outside of AI translation, formalization not capturing the spirit of what the informal description was provided is always a risk.

This is also a big risk when trying to prove code correctness: "prove this algo works" means you gotta define "works" along certain axes, and if you're very unlucky you might have a proof that exploits the uncertainty around a certain axis.