The problem that I want to see them tackle is formalizing the classification of finite simple groups.

Everyone uses the classification. Nobody has great confidence in the proof. Nobody understands it. There are attempts to reprove it.

If it can be formalized, that would demonstrate that AI is ready to formmalize all of mathematics.