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 insta

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! http://mathworld.wolfram.com/LookandSaySequence.html http://mathworld.wolfram.com/LookandSaySequence.html