*I should have clarified there is some proof generation, see the comment below by opnitro, but I meant the meat and potatoes of novel non-trivial proofs currently has to be supplied by the user.
A computer assisted proof is just as correct or helpful, it just may be more complicated of a proof initially. Given time said proof can be simplified but having the proof in the first place allows you to move away from assumptions into proofs or alternatively even open new doors that weren't known to exist.
Keep in mind that these computer aided proofs are equivalent to pen and paper proofs but because you can rely on software to guarantee you haven't made any mistakes, you can make more complex proofs that still work.
It's the same as with programming. You can write overly complex and opaque proofs in the same way you can write bad, slow, or hard to read code. It still "works" but it's not ideal and is often a first revision in a series of steps towards the clean, fast, and easy to read final products.