You have to pay close attention what system of logic the proofs are written in. So, for example, it is an open problem, how and whether proofs written in homotopy type theory can be interpreted computationally (source: http://en.wikipedia.org/wiki/Homotopy_type_theory#Computer_p...).