The fact of the matter is, if a proof exists, then a Curry-Howard version of the program exists too. That doesn't mean that it's easy to find, though.
Undecidability still holds for Curry-Howard: if your types are advanced enough to capture logic, then there's no algorithm which takes in a type and outputs a program of that type, if it exists. Just like there's no algorithm that looks at a proposition and tells you if it's true or not.
Billions of zeros on critical line have been calculated in many many ways.
Curry-Howard does not say that a program to compute zeroes can be turned into a proof of the Reimann hypothesis. It doesn't say that any program is a proof. What it says is, there is a dependently typed programming language where there's a type corresponding to the Reimann hypothesis, and a program with that type iff there's a proof of the Reimann hypothesis.
What this program would actually look like, if it's a proof, is a function that takes a number and a proof that that number is a zero of the Zeta function, and outputs a proof that that number is either a negative integer or has complex part 1/2. (Notice how the type of the input proof depends on the value of the given input, this is the "dependent" of dependent types).