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
Related questions
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