A few years ago the Notices of the American Mathematical Society ran a series of articles on the state of the art in using computer proof assistants. They are at least worth skimming.
"Formal Proof," by Thomas Hales
"Formal Proof - The Four-Color Theorem," by Georges Gonthier
"Formal Proof - Theory and Practice," by John Harrison
"Formal Proof - Getting Started," by Freek Wiedijk
I tend to be a traditionalist when it comes to traditional methods versus computer methods, but I do find arguments like the following compelling.
(This is from a news release from the AMS on their series of articles on formal proof.)
"When mathematicians prove theorems in the traditional way, they present the argument in narrative form. They assume previous results, they gloss over details they think other experts will understand, they take shortcuts to make the presentation less tedious, they appeal to intuition, etc. The correctness of the arguments is determined by the scrutiny of other mathematicians, in informal discussions, in lectures, or in journals. It is sobering to realize that the means by which mathematical results are verified is essentially a social process and is thus fallible." [emphasis mine]
(And this is from Hales's article.)
"The computer code that implements the axioms and rules of inference is referred to as the kernel of the system. It takes fewer than 500 lines of computer code to implement the kernel of HOL Light."
Verifying correctness on such a small program would be a lot easier than verifying correctness of proofs of many theorems.
(Also from Hales's article.)
"Experience from other top-tier theorem-proving systems has been that about three to five bugs have been found in each system over a period of 15-20 years of use. After decades of use on many different systems, to my knowledge, only one proof has ever had to be retracted as a result of a bug in a theorem-proving system, and this in a system that I do not rank in the top tier... We can assert with utmost confidence that the error rates of top-tier theorem proving systems are orders of magnitude lower than error rates in the most prestigious mathematical journals." [emphasis mine again]
As a side note, Hales's paper also lists several major theorems (already proved the traditional way, of course) that have been since proved by a computer. These include quadratic reciprocity, the prime number theorem, the fundamental theorems of algebra and calculus, the Jordan curve theorem, and the Brouwer fixed-point theorem.
Besides the Four-Color Theorem, apparently the Robbins conjecture was first proved by an automated theorem prover.
And, of course, there's Wikipedia on computer-assisted proof.