patternMinor
Why algorithms calculating non-tirivial zeros can't be used as proofs of Riemann Hypothesis?
Viewed 0 times
riemannwhyzeroscanhypothesisnonusedproofsalgorithmscalculating
Problem
Recently I was reading again this propositions as types paper by Philip Wadler:
http://homepages.inf.ed.ac.uk/wadler/papers/propositions-as-types/propositions-as-types.pdf
It gives an impression, that programs are proofs. So my first question was that why they are not enough for mathematical proofs then, for example in case of Riemann Hypothesis. Billions of zeros on critical line have been calculated in many many ways. I suppose they use some sophisticated algorithms or computer programs in that sense.
http://mathworld.wolfram.com/pdf/posters/Zeta.pdf
So, I was just stuck there. Why aren't these programs, or proofs in the system of Curry–Howard correspondence, enought?
http://homepages.inf.ed.ac.uk/wadler/papers/propositions-as-types/propositions-as-types.pdf
It gives an impression, that programs are proofs. So my first question was that why they are not enough for mathematical proofs then, for example in case of Riemann Hypothesis. Billions of zeros on critical line have been calculated in many many ways. I suppose they use some sophisticated algorithms or computer programs in that sense.
http://mathworld.wolfram.com/pdf/posters/Zeta.pdf
So, I was just stuck there. Why aren't these programs, or proofs in the system of Curry–Howard correspondence, enought?
Solution
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).
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).
Context
StackExchange Computer Science Q#85365, answer score: 6
Revisions (0)
No revisions yet.