This question is not precise, but I believe has a precise formulation. 


Consider a mathematical theorem which gives an equivalency between two conditions. As an extreme example:



> 
> **Theorem.**
>  A compact 3-manifold is simply-connected if and only if it is homeomorphic to the 3-sphere.
> 
> 
> 


The if direction is an exercise in a first course in algebraic topology, and the only if direction is a celebrated result of Perelman.


The question is, are there results which have been shown that one direction of a proof is "harder" than the other? 


Certain equivalence proofs seem to have the same complexity in both directions, when all the steps of the proof are reversible. 


I think this can be formulated as a precise way, by asking for the length of a proof in a standard proof system. One might also be able to give a precise formulation in terms of the Kolmogorov complexity of a proof. 


On the other hand, I can imagine results of the sort that say that for any equivalency, there is a proof system for which one direction is shorter than the other, and another proof system where the reverse holds. So I'm not certain that this question is well-defined. But I think it is well-defined for certain proof systems. 


So a more precise question: **Is there an equivalence theorem and a proof system, for which it has been shown that one direction of a proof must have a longer proof than the other direction?** 



Proof complexity of two directions of equivalency?
I think that there are numerous trivial examples of this. 


Take any implication $p\to q$ that is provable, but has no short proof. It follows that the equivalence $$q\leftrightarrow (p\vee q)$$ 
is also provable, and furthermore has a trivial proof in the forward direction, but no very short proof in the converse direction, since any such proof also gives a short proof that $p\to q$. 


