I thought there were several examples of theorems that had only been proved by computers, like the Four Color Theorem, but that they're sort of in their own universe because they rely on checking thousands of cases, and so not only could a person not really be sure that they verified the proof (because the odds of them making a mistake would be so high) they couldn't get much in the way of intuition or shared technique from the proof.
I thought there were several examples of theorems that had only been proved by computers, like the Four Color Theorem
Yes, although as far as I know things like that, and the FCT in particular, have only been proved by custom software written for the problem.
There's also a distinction between using a computer to find a proof, and using it to formalise a proof found by other means.
If it's worth saying, but not worth its own post (even in Discussion), then it goes here.
Notes for future OT posters:
1. Please add the 'open_thread' tag.
2. Check if there is an active Open Thread before posting a new one. (Immediately before; refresh the list-of-threads page before posting.)
3. Open Threads should be posted in Discussion, and not Main.
4. Open Threads should start on Monday, and end on Sunday.