Deciding isomorphism of simple groups, given by their multiplication tables. The fact that this can be done in polynomial time follows directly from the fact that all finite simple groups can be generated by at most 2 elements, and currently the only known proof of that fact uses the Classification of Finite Simple Groups (perhaps the largest theorem - in terms of authors, papers, and pages - ever proven).