I disagree with your statement and wish you would provide a counterargument. I think the four color theorem is an exception because mathematicians weren't impr

I disagree with your statement and wish you would provide a counterargument. I think the four color theorem is an exception because mathematicians weren't impressed and excited to find that computers could prove theorems. Instead they were disappointed and considered it somehow "wrong". We should be pushing forward with automatic theorem provers, and we would be if more mathematicians could program.