Comment by lupire

"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.