I don't really agree with that. Two examples come to mind: 1) Four color map theorem. I wouldn't have been horribly surprised if the code used to prove this

I don't really agree with that. Two examples come to mind: 1) Four color map theorem. I wouldn't have been horribly surprised if the code used to prove this made a mistake in 1,936 maps it had to check. Give that a second program verified it, I'd be more surprised now, but at the time, I would have been most worried about how to input the 1,936 maps. (I have no idea how this was done, if even generating them was programmatic, errors would have been less likely). 2) Automated symbolic logic programs are probably easy to make mistakes with. You need to have perfect parsing logic on the strings of each theorem and generate the new strings perfectly. I'm not saying its impossible, but mistakes are probably easy to make.