Solving SHA256 hash problems on Bitcoin is useful in the sense that secures the Bitcoin blockchain, but if your question is: "why can't it do something computationally useful as a side-effect?", then I think the answer is "we don't know how". For Bitcoin to work, the proof-of-work that miners do must have the following properties:
Cryptographic hash functions like SHA256 satisfy these four properties. I don't think automated theorem proving fits the bill because, as far as I'm aware, there is no way to prove how difficult it was to find the theorem that you proved. General purpose grid computing, like BOINC, doesn't fit the easy-to-verify requirement, at least in the context of Bitcoin. (In fact, I think this is an active area of research in grid computing, called the "cheating problem".)
If there some proof-of-work scheme that satisfies these four properties and also has some useful computation as a side-effect, that would be interesting. I'm not aware of any.