I vaguely remember from my undergrad that formalising all proofs isn't possible, due to axiom of choice making some issues (and if you decide to abandon axiom of choice, like in constructive mathematics, you lose real numbers).
It was a very interesting class, we mostly used Coq.
It was a very interesting class, we mostly used Coq.