A proof obfuscator is a program that takes as input a proof, and outputs a new obfuscated proof of the same theorem, such that the (distributions over) obfuscations of any two proofs of the same length are computationally indistinguishable.
The question is: does there exist a proof obfuscator that starts with a satisfying assignment to a 3SAT instance, and then produces a valid proof in ZFC that the instance is satisfiable?
This question resolves positively if at the end of 2024 there is any concrete candidate proof obfuscator for which I think there is a >10% chance of computational indistinguishability. (I won't accept if there is some Levin-search thing that maybe converges to indistinguishability for large input sizes---it needs to be some concrete strategy for obfuscating proofs that would have a signifiant probability of working on concrete proofs for merely astronomical constants.)
My expectation is that this is impossible. But note that circuit obfuscation is possible, and that there exist true axioms you can add to ZFC that would make proof obfuscation possible using existing techniques.
I give some more context on a Facebook post here: https://www.facebook.com/paulfchristiano/posts/pfbid02eEm5da6GEdqpJxtWi88e2cmKXNBVWUzrR27NZgNfMNfB8wkTetQeVt6JhETV6yiXl
1,000
3.00Seems to me this market could have resolved YES on the basis of the Groth Ostrovsky Sahai paper linked below. Is there some objection to that result from any @traders who bet NO in the intervening year?
@BoltonBailey The market creator seems to be saying multiple times that they don't know the norms of manifold - IMO the norm is that unless explicitly said otherwise, when a paper meeting the criteria of a market like this is located, the market resolves immediately. Perhaps this has been a cause of confusion?
@BoltonBailey The question as stated asks whether I would believe the proposal worked at the end of 2024. I wasn't fully confident about the resolution until the end of 2024.
(When we found the paper there was a significant probability that I was misunderstanding or overlooking some subtlety. Over time that probability fell; I'm not sure if there is a norm that I am supposed to resolve the market when I get to some threshold of confidence. I don't know where that threshold would be, and it didn't seem like there was any particular reason to resolve early.)
does there exist a proof obfuscator that starts with a satisfying assignment to a 3SAT instance, and then produces a valid proof in ZFC that the instance is satisfiable
Wouldn't a solver that does not use the witness at all and just solve the 3SAT instance from scratch (even if in exponential time) trivially meet this definition?
@Sg97 the market creator created the market because no one else did. Markets are typically created by people who are interested in the opinions on the question. He's now trading according to his beliefs. Don't trade if you don't want to, but please don't spam.
@firstuserhere I don't know norms around this kind of thing on manifold, am happy to be corrected if there are norms about e.g. closing a market rather than trading once the answer seems pretty clear. The main weird thing here is that someone came in with a 2k subsidy ($20?) while the market was at a low probability.
Manifold norms are that betting in your own markets is fine so long as you're actually predicting, even if you're ten seconds away from resolving the market yourself and betting it all the way to 1/0. I think maybe we should discourage the last one a bit more than we do, but currently everyone does it. What you've done is totally fine.
This paper from 2006 appears to use pairings to give witness indistinguishable proofs with provably perfect soundness. If you combine a WI proof in this system with a soundness proof from this system, then you get an obfuscated proof. It's a pretty big result that's been out for a long time so I don't think it's wrong. https://web.cs.ucla.edu/~rafail/PUBLIC/73.pdf