Unfortunately, even simple undergraduate proofs can be monumentally difficult or even impossible to translate into a type theory due to inherent limitations of the theory or the type checker.