I suppose that this would turn on what you mean by "vouching" for a proof. It seems to me that using a computer-generated proof would require a proof of soundness of the program.