What paradigm of automated theorem proving is appropriate for Principia Mathematica-style formalization?
Several points:


As far as I know, Principia Mathematica uses essentially a formalization of set theory using a typed first order logic. It would therefore be tempting to use a first-order automated theorem prover like Prover 9 or possibly ACL2 to formalize your statements. However, I am seeing several set-theoretic constructions (like $\in$, $\cap, \subset$) in there, which usually don't play very well with first order ATP.
Any modern interactive proof assistant will surely have the expressiveness to formalize and prove your statements, as Andrej has suggested. In fact, since there seem to be some statements including arithmetic, it would be wise to use a system like Isabelle, Coq or HOL which already have extensive theories to treat statements of arithmetic. My emphasis on modern is not a coincidence: great strides in usability have been made since Automath, and I honestly think you would be doing yourself a disservice by using anything that hasn't been actively developed since the 90's (if you could even get one to work!)
Finally, ITP and ATP have rather challenging learning curves, and you shouldn't expect to be able to enter these theorems into such a system as if you were writing a $\LaTeX$ proof. Expect severe frustration and lost time, especially in the first months (yes, months). You definitely need to work through some tutorials at first before getting to the main formalization.