There are probably many reasons for the difficulty, but there might be one particularly difficult problem: Mathematicians may be using meta-induction instead of induction leading to erroneous proofs.
Bundy et al. in "What is a proof?" claims that S. Baker in "Aspects of the constructive omega rule within automated deduction" claims that often when mathematicians claim to do induction they actually do meta-induction. This means that instead of proving $\forall n. P(n)$, they instead end up proving $\forall n:{\mathbb N}. Provable(P(term(n))$ (i.e. $P(0), P(1), \ldots$). This result is, in general, weaker that the result $\forall n. P(n)$ that they claim to be proving. The paper proofs are so informal that it is hard to tell that this is what they are doing, and this coupled with the fact that the theorems they are claiming to prove are actually true (and provable), means that this subtle error goes unnoticed. This leave formalizers with the difficult task of providing an actual inductive proof.
Thanks to schropp for pointing this out. Sorry for stealing your Mathoverflow karma.
