"Informal to formal" is harder than "formal to formal". These puzzle problems are quite simple (for computers) if you have a formalization.
"Informal to informal" is so far snake oil.
"Informal to informal" is so far snake oil.
That may be true someday, but it's not yet! That's exactly what the IMO Grand Challenge is about, and nobody has gotten close to solving it.
As far as I know, based on published systems like LeanDojo [1] and Magnushammer [2], computers today can only solve a small handful of the very easiest of these problems (like maybe Imo1959P1).