A computer program would have to be debugged. Lots of proofs are done by proving an algorithm works and applying the algorithm to a given idea. But if there's a bug in the program, how do you find it? It's rare that a computer program can be checked at the level of a proof.
What computers can often do is generate data that suggests a plan of attack for the general proof. I'm not saying that they aren't extraordinarily helpful. Bredan McKay in Australia makes a good living checking things with computers. But once the computer finds something, he has to write a conventional proof.
You can "prove" combinatorial identities until you die, but that doesn't make it a general, applicable theorem.
As you have pointed out, tree search is employed to prove mathematical theorems these days. This is economical because humans are unlikely to find proofs that aren't, in some manner, elegant. When mundane brute force is called for in proof, computers excel because humans can't stand to do it, and don't have the bandwidth.
Searching for interesting provable theorems is something else again, and, as you say, computers aren't as good as humans. However, computers are not entirely out of the running. We found two theorems by computer search, in spherical geometry, that were, in fact, employed by astronomers. Other people, over the years, have found other useful minor theorems, using similar programs. So it's not really true that computers don't find useful theorems, it's just not presently a very valuable, or cost efficient way to find theorems. It was a pretty viable way for CS students to grab a doctorate. I imagine it may be considered a little too mundane to leverage a doctorate with these days.
A computer program would have to be debugged.
And a human would have to follow a proof, and humans are fallible, and notorously resistent to debugging.
Lots of proofs are done by proving an algorithm works and applying the algorithm to a given idea. But if there's a bug in the program, how do you find it?
I think you have the cart before the horse. For the interesting bugs, The only way you know there's a bug in a program is to apply it to the real world. Most interesting bugs have to do with specs that are inadequate to the field of discourse. A provably correct program could still easily have a bug. If there's a bug in a program you redo the software and start the proof over from scratch. And then you will have a new provably correct program, which may easily still have a bug.
It's rare that a computer program can be checked at the level of a proof.
It's rare to unknown that a provably correct program still doesn't suffer from many bugs when the development team finally decides to quit wasting its time trying to generate a perfect program and ships before they all get fired.
Proof isn't the germane challenge in getting useful software out--We've had provable programming systems, arising from Lisp, Prolog, and the Wirth/Dykstra contribution, that I know of (there are probably others). And it's no more or less of a challenge to be absolutely convinced that your compilers produce proofworthy code, as it is to convince yourself that formal systems of proof are in fact, correct. Amusingly enough, syllogistic logic was formulated with two "bugs" by Aristotle, and this wasn't caught until the beginning of the 20th century. Sort of an inverse testement to just how useful logic actually is in daily life, or math, for that matter. Treating programs as if they were proofs added lots of expense, and little by way of value to the software production process. The real world is not a subset of math.
Math is a partial subset of the real world, which is sometimes quite useful, and sometimes a enormously expensive waste of time. Knowing the difference is important, and for that, you need humans, with feelings about analytically intractable things like love and duty and beauty and ambition, not mathematically tractable algorithms.