and we don't have 100% accuracy in translation in ambiguous texts, because system often need some domain knowledge, context etc. And math has 0% tolerance to mistakes.

I also expect that math formalized by machine will be readable by machine and hardly understandable by humans.