There's a difference in math between giving just the answer to a problem and doing it properly/elegantly.
So yeah, generated machine-valid proof can be denied if it's incomprehensible, same as human machine-valid proof can be denied for same reasons.
there is a difference but it's overrated. if a theorem is proven, then, as OP said, the theorem is the interface, no matter where the proof is.
just as we don't re-prove Fermat's little theorem every time I use it in a proof, because well, it's a theorem.