I think that, if you are wanting a formally verified proof of some maths theorem out of the oracle, then this is getting towards actually likely to not kill you.
Yes, I believe that’s within reach using this technique.
You can start with m huge, and slowly turn it down, so you get a long list of “no results”, followed by a proof. (Where the optimizer only had a couple of bits of free optimization in choosing which proof.)
This is quite dangerous though if the Oracle is deceptively withholding answers; I commented on this in the last paragraph of this section.
Yes, I believe that’s within reach using this technique.
This is quite dangerous though if the Oracle is deceptively withholding answers; I commented on this in the last paragraph of this section.
If the oracle is deceptively withholding answers, give up on using it. I had taken the description to imply that the oracle wasn’t doing that.