How do researchers go about proving uniformity of proposed hash functions? Is it just an empirical matter of running many inputs through the function and observing the distribution of outputs, or can one formally prove the property? Where could one (non-crypto-expert) learn about how such proofs are constructed and look one up e.g. for the case of SHA-256?
Uniformity is a tricky one. SHA-256 (as well as SHA-3 for that matter) follows a heuristic approach. That is, the design is not based on a hardness assumption (for example, the factoring or discrete-log assumption) but on criteria that have only been verified empirically. As such, also the study of uniformity is an empirical study. The development of SHA-1/SHA-2 was not a public process (it was developed by the NSA and NIST) and no rationale as to design choices were given. What you usually do in this case is to run statistical tests and see if any of them indicate any weaknesses. For example, a simple test would check that every single output bit is set to 1 with probability 0.5. A suite of statistical tests that, I believe, was used in the evaluation of AES was published by NIST (http://csrc.nist.gov/groups/ST/toolkit/rng/documentation_software.html).
If you want to go into more detail I would have a look at the SHA-3 competetion. Here, every candidate had to provide an elaborate and convincing case for why this candidate is a good pseudorandom function. You can find the documents for Keccak (the new SHA-3) on http://keccak.noekeon.org/files.html. The Keccak reference has a whole section on the analysis of Keccak as a pseudorandom function.