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:

\begin{theorem} A compact 3-manifold is simply-connected if and only if it is homeomorphic to the 3-sphere. \end{theorem} 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?**

lengthof a formal proof is not a very interesting metric, because we don't normally look at formal proofs anyway (so the length is meaningless for practice) and because the length depends as much on the proof system as on the theorem being proved. Reverse Mathematics can capture the set-existence axioms required for each direction. But trying to capture how "easy" or "natural" each direction is to prove is a challenge that has not been solved. – Carl Mummert May 17 at 21:03