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.
The theorem doesn't exist in a vacuum. It talks about objects that must be formally defined. And if that formal definition (which is part of the API) is not immediately compatible with those others use, and every single theorem comes with its own definitions of the objects they're working on, you're going to be reinventing the wheel over and over again.
Replacing thought and curation with repeated automation is tech debt, pushed down to fundamental knowledge and understanding.
> just as we don't re-prove Fermat's little theorem every time I use it in a proof
Exactly! There's a shared foundation, and everyone builds upon it. A mathematical paper is a whole bunch of Lego blocks being added to that foundation, and combining them in a hopefully-useful new interface.
But if the entire paper is just one giant black box, you only get to use the final interface: you lose the ability to meaningfully repurpose the individual Lego blocks to build a different interface. You end up having to reinvent the same Lego blocks over and over again, just with a slightly different color each time.
Don't want to re-prove each and every Lego brick? Then you shouldn't accept giant black box proofs.