I was reading Scott Aaronson's blog, and one of the comments sparked a question.
"if P!=NP, this would be a general, conceptual result, so you’d expect the proof to be explanatory and in particular human-scaled. If P=NP, it could be 'an accident' and the reason is simply that there is some astronomic but polynomial time algorithm for SAT, an algorithm which humans might never grasp."
Problems with this specific argument aside, it seems that many proofs are best made by counterexamples, and often these counterexamples are simple enough that it's possible they could be semi-randomly generated by a computer, then automatically checked (say with an Interactive Proof).
This is also true with algorithms - there are many procedures for checking if an algorithm works for solving a problem (IE: Blum and Kannan's procedure for the Graph Isomorphism Problem) efficiently, without providing the algorithm itself.
I recognize you have many approximation algorithms that use this very principle to give near/if not optimal answers, but I'm asking about the case where typically such a search isn't academically productive because of how uncommon a randomly generated correct result occurs.
Are there any significant proofs/efficient algorithms that have been randomly generated, potentially far ahead of the theoretical understanding for why those counterexamples exist? Or provided a helpful background that created motivation for building the knowledge-base for that understanding?
The main reason I'm asking is because I've never head of such a result, and am wondering how commonly this occurs (thus if it's a viable assumption it can occur).