Does there exist an indistinguishability formal proof obfuscator?
Since you do not give $T$ as an input, the existence of such an $\mathcal{O}$ seems

like it should significant constraints on the is_a_proof_of relation:

For example, if there are proofs P0,P2,P1 and Theorems T0,T1,T2 such that

[for all elements i and j of {0,1,2}, ​ Pi is_a_proof_of Tj ​ if and only if ​ i ≠ j ]

then there would have to be a P such that P is a proof of all three of those theorems.




  For the rest of this answer, assume there is a function theor_of_ such that
  
  for all proofs P and theorems T, if P is a proof of T then ​ theor_of_(P) = T .




Under that assumption, sure. ​ ​ ​ For such a function theor_of_, one can

have $\mathcal{O}$ be given by ​ ​ ​ $\mathcal{O}(P)$ ​ = ​ lexicographically least proof of theor_of_(P) ​ .

That $\mathcal{O}$ is in Ptheor_of_[1],NP.

You probably want $\mathcal{O}$ to be efficient, or at least significantly faster than brute force for suitable input lengths, even if NP is hard. ​ For that requirement, it becomes very significant that

you do not give the security parameter as input
and
you're not relating the lengths of the proofs

.
The distributions thus do not depend on the security parameter, so if they're indistinguishable then they're identical. ​ Efficiency in particular forces output-length to be not so much longer than input length, so for the resulting distributions to be identical, $\mathcal{O}$ must find a proof which is not so much longer than the shortest proof, regardless of how long its input proof is.

The latter is the much stricter requirement - For example, consider statements of the form "There exists an x such that $\big[\big[$x satisfies $\phi \big]$ or [length(x) = L]$\big]$", and proof systems for which the proofs of such statements are exactly ordered pairs of the statement and such an $x$.

By setting L so that it will be slightly greater than

$\big[\mathcal{O}$'s runtime on proofs of the resulting formula for which $x$ is a satisfying assignment$\big]$ (remember that L is only log(L) bits long) and giving $\mathcal{O}$ a proof with an L-bit $x$, $\mathcal{O}$ must solve $\phi$.

Even for proof systems that are not so insistent on constructiveness, one could try

replacing ​ length(x) = L ​ with something else such that $\big[$one also gets a proof but it's

probably hard to find a proof that's not sufficiently longer than assignments to $\phi \big]$.

Even if you [give the security parameter as an input] and [only require indistinguishability against uniform adversaries that must choose equal-length proofs], such an $\mathcal{O}$ for a

similarly-constructive proof system would suffice for inverting candidate one-way functions with probability greater than 1/3 ​ - ​ Just run it on proofs that give r for statements

"There exists an x such that f(x) is in {$\hspace{.02 in}$y,z}.", where a random one of

of y,z is the target image, the other of them is f(r), and r is chosen

uniformly from strings with length equal to the security parameter.

Thus, if one-way functions exist then for a feasible such $\mathcal{O}$ to exist,

the proof system must not be feasibly constructive.





Now, I'll finally give the positive results:



As warmup, if there is an efficient non-interactive witness-indistinguishable proof system

NIWIP for SAT with deterministic verifier, then for axiomatic systems S such that

a theor_of_ function, as described near the top of this answer, is efficiently computable
and
the proof system includes arithmetic and

[can prove enough about its own provability predicate]
and
there is a poly(k,M)-time algorithm for finding a proof in ​ S + Con(S) ​ that

NIWIP with security parameter k is sound for statements of length at most M

then there is an efficient $\mathcal{O}$ that takes as input

the security parameter, in unary
and
a length bound L, in unary
and
a proof in S of a $\Pi_1$ formula

and outputs a proof in ​ S + Con(S) ​ of the same $\Pi_1$ formula,

such that the desired indistinguishability will hold when

the security parameters are equal
and
the length bounds are equal
and
the proofs both satisfy the length bound

.
Furthermore, if NIWIP's indistinguishability is perfect,

then $\mathcal{O}$ does not need the security parameter.

(In either case, use NIWIP on the existence of a proof of length at most L, prove the relevant

soundness property of NIWIP to deduce the existence of a proof in S of the $\Pi_1$ formula, and

then use Con(S) and [provable-in-S facts about being provable-in-S] to deduce the $\Pi_1$ formula.)

It's finally time for the full result. ​ For axiomatic systems S0 such that

a theor_of_ function, as described near the top of this answer, is efficiently computable
and
the proof system includes arithmetic and

[can prove enough about its own provability predicate]

, ​ ​ ​ with the axiomatic systems ​ S1,S2,S3,S4,...,S$_{\infty}$ ​ given by

Sn+1 is Sn plus [the schema with one axiom per wff p, where those

axioms are padded (for example, by ANDing with 0=0) to each be longer

than n bits, and otherwise just assert "if p is provable in Sn then p"]
and
S$_{\infty}$ ​ = ​ S0 + S1 + S2 + S3 + S4 + ...

, if there is $\big[$an efficient non-interactive witness-indistinguishable proof system NIWIP for SAT with deterministic verifier$\big]$ and $\big[$a poly(k,M)-time algorithm for finding a proof in S$_{\infty}$

that NIWIP with security parameter k is sound for statements of length at most M$\big]$,

then then there is an efficient $\mathcal{O}$ that takes as input

the security parameter, in unary
and
a length bound L, in unary
and
a proof in S$_{\infty}$

and outputs a proof, also in S$_{\infty}$, of the same formula,

such that the desired indistinguishability will hold when

the security parameters are equal
and
the length bounds are equal
and
the proofs both satisfy the length bounds

.
As before, if NIWIP's indistinguishability is perfect,

then $\mathcal{O}$ does not need the security parameter.

(In either case, work as follows: ​ ​ ​ Proofs in S$_{\infty}$ of length at most L cannot use axioms that aren't in SL, so use NIWIP on the existence of a proof in S$_{\infty}$. ​ From there, prove the relevant soundness property of NIWIP to deduce the existence of a proof in SL of the relevant formula, and then use the relevant axiom from SL+1 to deduce the relevant formula itself.)



I'm not aware of any candidates for that which Shor's algorithm won't break.