> Formalization is in principle just a translation process and should be a much simpler problem than the actual IMO problem

maybe not, because you need to connect many complicated topics/terms/definitions together, and you don't have a way to reliably verify if formalized statement is correct.

They built automatic formalization network in this case, but didn't trust it and formalized it manually.