The problem might be that once you try to get your theorem into a proof system, you're not doing maths anymore: now you're programming.
Programming is a whole discipline apart from mathematics. It's grounded in mathematics, but in practice it really is engineering. There are myriad choices to be made, most of little or no mathematical significance. Just managing names becomes a task; using the same Hebrew letter to mean five (more or less analogous) things in one proof becomes impossible. Maybe even using a Hebrew letter is hard.
Mathematicians who wanted to be programmers might be programmers already. Mathematicians willing to do engineering might be engineers already.
We have lots of experience with physics grad students writing unmaintainable spaghetti code to analyze experimental result data. It is tolerable because the code is more-or-less discarded after the paper is published. But this code is supposed to support all of the future of mathematical development, forever.
Who will rewrite the shoddy parts when their (practical) flaws become intolerable? Will it even be possible, with the weight of decades depending on it? What abstraction methods does the language offer to help decouple the statement proven from the expression of its proof?
Very often the lemma your proof depends on isn't exactly what somebody else proved, but something analogous. Mutatis mutandis, it's the same, conceptually, but that's not good enough for your proof system.
Do you want dozens of almost-identical proof statements in the system? Is the language strong enough to unify them? Does unifying them count as doing maths? It will usually feel more like engineering.
Other software engineering considerations become important, notably runtime performance. Is a proof acceptable if it would take a hundred years to evaluate, so hasn't been? Can it be parallelized? Who provides the equipment to do it?
