Proving a known zero of the Riemann Zeta has real part exactly 1/2

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.

First, one uses the argument principle from complex analysis to compute the number of zeroes with real parts between $0$ and $1$ and with imaginary parts between $0$ and some positive number $T$. Since the answer is a priori an integer, one can get a precise answer even though one can't compute the $\zeta$-function exactly; it is "just" a matter of bounding the error in all approximations carefully enough.

Then, one has to show that this number of zeroes actually lie on the line where $\Re s = 1/2$. For this, one factors $\zeta(1/2 + i t)$ as a product of a certain nowhere zero function, and a real valued function $Z(t)$ (the function appearing in J.M.'s answer). (That this can be done in a useful way is part of the theory of the $\zeta$-function.)

To count zeroes of $\zeta$ with $\Re s = 1/2$ is now the same as counting zeroes of $Z(t)$, which can be determined by sign changes in $Z(t)$ (provided one estimates $Z(t)$ accurately enough).

Assuming that all works out (which it will if RH is true!) one gets a rigorous proof that all zeroes with imaginary part $\leq T$ lie on the line $\Re s = 1/2$. (In fact, for this to work out, one also needs the zeroes of $\zeta$ to be simple, which they are conjectured to be; see T..'s answer for an elaboration on this.)

From what I've found, it's mostly presented as a fait accompli, for instance, the Riemann-Siegel function $Z(t)$, a function frequently used in the zero-finding, is defined with a $\zeta\left(\frac12+it\right)$ factor. What now one looks for when using constructs like these is if the function ever "turns away" from the horizontal axis without crossing it (if this does happen, the hypothesis is false).

This is why things like Lehmer's phenomenon are interesting behavior for the ζ function. Put simply, these are sections of the critical strip where there is (very!) nearly no crossing.

Here are two traditional ways of visualizing the Lehmer phenomenon: one can look at the graph of the Riemann-Siegel function:

(Mathematica code: Plot[RiemannSiegelZ[z], {z, 0, 100}, AspectRatio -> 1/5, Frame -> True])

or the so-called "zeta spiral" $z(t)=\zeta\left(\frac12+it\right)$ in the complex plane:

(Mathematica code: ParametricPlot[Through[{Re, Im}[Zeta[1/2 + I t]]], {t, 0, 40}, AspectRatio -> Automatic, Frame -> True]).

Now, here is the first instance of the Lehmer phenomenon, seen using both viewpoints:

(Mathematica code: Plot[RiemannSiegelZ[z], {z, 7004, 7006}, Frame -> True, PlotRange -> {-2, 2}])

(Mathematica code: ParametricPlot[Through[{Re, Im}[Zeta[1/2 + I t]]], {t, 7004 + 1/2, 7005 + 1/2}, AspectRatio -> Automatic, Frame -> True])

The hypothesis would have been false if for the Riemann-Siegel function, the function displayed a local extremum without crossing the x-axis, or for the zeta spiral, the apparent "cusp" was actually a cusp or did not even pass through the origin. (I won't spoil the fun by posting zoomed-in versions of those last two images, you can do it yourself with Mathematica or some other computing environment that can evaluate ζ(s) for complex values).

The two zeroes are in fact quite close: FindRoot[RiemannSiegelZ[x], {x, ##}, WorkingPrecision -> 20] & @@@ {{7005 + 1/50, 7005 + 7/100}, {7005 + 9/10, 7005 + 11/100}} returns the two approximate zeroes 7005.0628661749205932 and 7005.1005646726748389.