3 ms·
It reminded me of what Dr. Doron Zeilberger has been repeating ad-nauseam ( eg: http://www.math.rutgers.edu/~zeilberg/Opinion36.html http://www.math.rutgers.edu
by dxbydt 15y ago
It reminded me of what Dr. Doron Zeilberger has been repeating ad-nauseam ( eg: http://www.math.rutgers.edu/~zeilberg/Opinion36.html 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.
- nandemo 15y agoBut 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! http://mathworld.wolfram.com/LookandSaySequence.html http://mathworld.wolfram.com/LookandSaySequence.html