verifying proof for riemann-hypothesis is not harder than generating one, but say if you have access to one alleged-proof of riemann-hypothesis which is long enough such that verifying itself is super-hard, then you have no evidence to say that the proof is correct unless you prove that the AGI generating the proof is indeed capable of generating such a proof and being honest to you.
verifying a proof may run in polynomial time compared to the exponential of finding one, but it doesn’t rule out the possibility that there exist a large enough proof which will be hard to check.
There are many algorithms which are polynomial in time but are far worse to run in reality.
Thinking about this a bit more, it’s theoretically possible that the AGI has some high level proof that expands recursively into an almost infinite number of lines of some lower level formal language.
Presumably then the solution is to get the AGI to build a theorem prover for a higher level formal language, and provide a machine checkable proof that the theorem prover is a correct, and so in recursively till you can check the high level proof.
Also, the AGI can generate a long valid proof but it may not be for the question you have asked, since the assumption is that the problems described in natural language and its the AGI’s job to understand and convert it to formal language and then prove it
I think instead of recursively asking for higher level proof it should be a machine-checkable regarding the correctness of the AGI itself?
verifying proof for riemann-hypothesis is not harder than generating one, but say if you have access to one alleged-proof of riemann-hypothesis which is long enough such that verifying itself is super-hard, then you have no evidence to say that the proof is correct unless you prove that the AGI generating the proof is indeed capable of generating such a proof and being honest to you.
Verifying a proof is so much cheaper than finding it, that if it’s expensive to verify a proof, the proof is certainly wrong.
verifying a proof may run in polynomial time compared to the exponential of finding one, but it doesn’t rule out the possibility that there exist a large enough proof which will be hard to check.
There are many algorithms which are polynomial in time but are far worse to run in reality.
Certainly such a proof could exist, but it’s impossible for an AGI to find it.
Thinking about this a bit more, it’s theoretically possible that the AGI has some high level proof that expands recursively into an almost infinite number of lines of some lower level formal language.
Presumably then the solution is to get the AGI to build a theorem prover for a higher level formal language, and provide a machine checkable proof that the theorem prover is a correct, and so in recursively till you can check the high level proof.
Also, the AGI can generate a long valid proof but it may not be for the question you have asked, since the assumption is that the problems described in natural language and its the AGI’s job to understand and convert it to formal language and then prove it
I think instead of recursively asking for higher level proof it should be a machine-checkable regarding the correctness of the AGI itself?