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