It reminded me of what Dr. Doron Zeilberger has been repeating ad-nauseam ( eg: http://www.math.rutgers.edu/~zeilberg/Opinion36.html )
Ultimately automated theorem provers are going to rule. Dr.Z actually takes the very radical stand of calling all paper-pencil math proofs of Paul Erdos trivial, whereas "Theorems that only computers can prove...are not quite as trivial". The fact that we have to reach out to a computer to assist in solving min-sudoko is unfortunate but at the same time, inevitable. Dr. Z mentions Four Color Theorem, Kepler's Conjecture, and Conway's Lost Cosmological Theorem as other theorems only computers can solve.
But note that the proofs for the 4-Color Theorem and this Sudoku theorem are "merely" computer-assisted. The part of reducing the Sudoku search space, for instance, seems to have been done pencil-and-paper style. What Zeilberger wants is completely automated proving.
Oh, and thanks for introducing me to Conway's Cosmological Theorem. Very interesting!
