In math, the utility lies in the proof itself. A novel proof of a hard problem usually comes with new insights and abstractions that help solve even more mathematical problems.

To go with your analogy, mathematicians care more about the source code of the program than about the result of the program. But I'm afraid that we will see things change with the increase of vibecoded proof slop. A black box proof is not as useful, even if it is correct.