If you are interested in the underlying goal of Principia Mathematica, I urge you to check out the Metamath Proof Explorer (MPE): https://us.metamath.org/mpeuni/mmset.html
By itself, Metamath doesn't have built-in axioms. MPE uses Metamath to first state a small set of widely-accepted axioms, namely classical logic and ZFC set theory, and then proves a tremendous amount of things, building up to a lot of mathematics from careful formal proofs that rigorously prove every step.
Some things cannot be proven, but that doesn't mean that proof is dead.
Don’t get me wrong, PM is marvelous and there’s no gainsaying its enormous historical impact.
If your characterization of Metamath is correct, I don’t think that’s in the spirit of PM at all. One of the major problems PM had was the rejection of (what later became) the Axiom of Choice in favor of Russell’s convoluted theory of types. Indeed, that set theory (ZFC) is needed to get the rest of the way R&W were trying to go is one of the signal failures of the logicist program behind PM.
However, if you think the main point of Principia Mathematica was the very specific set of axioms that they chose, then that's different. The PM authors chose to use a "ramified" theory of types, which is complex. It does have sets, it's just not ZFC sets. Few like its complexities. Later on Quine found a simplification of their approach and explained it in "New Foundations for Mathematical Logic". There's a Metamath database for that "New Foundations" axiom set as well (it's not as popular, but it certainly exists): https://us.metamath.org/index.html
More Metamath databases are listed here, along with some other info: https://us.metamath.org/index.html
The elementary vernacular foundations of modern mathematics is (more or less) naive set theory; the starting tools of serious foundational work (as arcane as it is even within maths as a whole) are logic and more rigorous set theory, perhaps with some computability mixed in; the main tool of a mathematician who wants to reason in great generality is category theory (with some handwaving in the direction of the previous point about universe hierarchies and whatnot). There are some signs of convergence between these (and of mainstream mathematicians starting to once again take foundations seriously), but at the basic level those are what you’ll be dealing with.
None of them existed in their current form at the time PM was written, even logic (no Kripke semantics! no forcing! and no Gödel of course). Some did not yet exist at all. Some changed quite drastically in direct response to PM. And of course PM is the origin of (embryonic) type theory, which is the inspiration of the unified approach I referenced above. So as a historically important text, sure, if that’s what you want, but as a gateway to understanding more interesting maths it’d be terribly inefficient.
In that respect TAoCP was uniquely lucky. It was also a self-obsoleting book: it ceased to be comprehensive months after it was published, exactly because it told you everything there was to know about algorithms to date. Yet none of the stuff that’s in it is itself obsolete, there’s just immesurably more stuff now. PM, on the other hand, was attempt at “rationalization” in the 19th-century sense, and mostly a failed one except for serving as fertilizer for all of the later ones.
