Conway's opposition was to computer-generated proofs (not computer-verified proofs), because the software of the time wasn't high quality (for accuracy), and be

Conway's opposition was to computer-generated proofs (not computer-verified proofs), because the software of the time wasn't high quality (for accuracy), and because they were so complicated that people couldn't get confidence that they were debugged. Basically, humans can't comprehend what the computers are doing, even when they are right, and we aren't always building them well enough to be trustworthy without checking their work. However, Zeilberger and Shalosh B Ekhad have done some highly reputable work, albeit in a narrow area. (Zeilberger designs algorithms in combinatorics, which then computer-generate proofs for specific questions) http://www.nytimes.com/learning/teachers/featured_articles/20040406tuesday.html http://www.nytimes.com/learning/teachers/featured_articles/2...