Comment by cperciva

Proofs at this level are nowhere near formal enough for existing mechanical tools to understand. I've seen researchers cite "translated proof X into an automatically-verifiable form" as a major achievement -- even for very simple proofs.