Comment by Someone

> But proving the object exists is still useful, of course: it effectively means you can assume an oracle that constructs this object without hitting any contradiction.

I don’t think that logic holds in mainstream mathematics (it will hold in constructive mathematics by definition, and may hold in slightly more powerful philosophies op mathematics) because there, we can prove the existence of many functions and numbers that aren’t computable.