Moreover, no one really knows how hard it is to compute a valid block. The trial-and-error method used by miners is just the most efficient method that we know; but there is no proof or other evidence that there is no better way.
Would you consider the fact that nobody has ever found a collision of sha256 function an evidence? There's no mathematical proof, but there's more then enough evidence that any other method is not even on the horizon. It's not only a Bitcoin issue, if any of modern hash algorithms would be compromised the whole cryptography would be hammered.
I believe is is proved (perhaps, I haven't checked) that the output values of SHA256 span all possible 256-bit strings or at least a very large subset of them (say, 2^200 strings). On the other hand, it is obvious that, if the inputs are 1000-bit strings, no mater how SHA256 is used there will be 2^(1000-256) = 2^744 input strings that have exactly the same hash.
Having a large output set is the very minimum requirement for a hash function. However, even stupid functions like "take the first 256 bits of the input" will have that property. If a function has that property, it will pass the simple collision test "generate N random input strings, compute their hashes, and look for duplicates". That is because N must be MUCH smaller than 2^256, so the chance of catching a collision is small -- if N = 2^56 = 72 quadrillion, the chance of finding a collision (that certainly exists, if the input has more than 256 bits) is only 1 in 2^200.
SHA256 has passed much more interesting tests, like "take N random texts, make M slighlty modified copies of each, compute their hashes, and look for duplicates". But, again, many simple functions pass this test too. (These functions may still be good checksums, suitable to detect non-malicious changes in files; or in hash tables, where malicious inputs are not expected.)
The property that makes a function be a good
cryptographic hash function is: "there is no algorithm that, given a text X, will find another text Y with the same hash as X in a viable amount of time". That property has not been proved, because there is no theory that would enable such proofs; and cannot be tested, because it would require trying all possible algorithms, and then testing each one to see whether it works. All that can be said is that many smart people have tried to find such an algorithm, and no one has succeeded
(that we know of).