Much effort has been expended on a famous unsolved problem about the Riemann Zeta function $\zeta(s)$. Not surprisingly, it's called the Riemann hypothesis, which asserts:
$$ \zeta(s) = 0 \Rightarrow \operatorname{Re} s = \frac1 2 \text{ or } \operatorname{Im} s = 0 .$$
Now there are numerical methods for approximating $\zeta(s)$, but as I understand, no one knows any exact values except at even integers, which include the trivial zeroes for which $\operatorname{Im} s = 0 $. So I've always wondered: For the rest, how does one prove $\operatorname{Re} s = 1/2$ exactly?
(All I know that seems vaguely useful is the argument principle, which I'm not sure helps here, but I'd be happy to learn about other techniques that aren't too far advanced.)
Edit: Looking over this again, I found out I missed the closed-form values at odd negative integers. This doesn't affect the question but seemed worth correcting. Thanks to the people who contributed.




As long as there are no multiple zeros on the line up to height $T$ you can determine, rigorously and using a finite amount of computation:
the number of zeros (counted with multiplicity) off the critical line, i.e., the number of counterexamples to the Riemann hypothesis, of height less than $T$. This is done by contour integrals of $d \log \zeta$ -- the "argument principle" in complex analysis. For each zero one can locate it to any specified accuracy, and determine its multiplicity.
the number of zeros on the critical line, up to height $T$. For each zero, its ordinate on the line can be calculated to any desired accuracy. This is done by counting sign changes of real-analytic functions with a $\zeta (1/2 + it)$ factor, on the critical line. As Matt E mentioned, the ability to write down a real-valued function capturing the behavior of a complex function on a line is a special phenomenon particular to zeta and L-functions, coming from the functional equation relating $\zeta(s)$ to $\zeta(1-s)$.
If there is a multiple zero of order $n$ at some point on the line, all you can determine by computations of the above type is that a very small neighborhood of that point contains $n$ zeros (counted with multiplicity). This could mean zeros on the line, counterexamples to the Riemann conjecture, or both.
It is part of the package of conjectures surrounding the Riemann hypothesis, that there are no multiple zeros, and that the zeros in fact "repel" each other in a quantifiable sense. There is a lot of numerical and theoretical support for the zero repulsion, especially from random matrix theory. If the Riemann hypothesis is true but there are multiple zeros, that would be almost as surprising as finding a zero off the line.