It wouldn't be quite so bad if there were a huge repository of already proven theorems you could pull from. But in reality you'll probably find yourself defining what a Turing machine is, what asymptotic complexity is, deriving results like the master theorem, and a thousand other trivialities you would just skip over in a paper.
It is especially problematic that there isn't a common repository of reference implementations of well-known unproved propositions. It would be so easy to make a subtle mistake in your definitions that allowed an existence proof to go through in a way that wouldn't generalize to the actual definition. For example, when you define probabilistic computation, if you declare that a probabilistic gate is a stochastic matrix with real number entries, you will incorrectly find that there exists probabilistic programs that solve the halting problem.