Comment by dwrensha

> These puzzle problems are quite simple (for computers) if you have a formalization.

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.