[mdup]

No, I don't think MetaMath is the kind of thing the OP wants. Sure, it builds mathematics from "first principles", but not in the same meaning as the OP means. When you read his question, "first principles" really mean "as a beginner".

Although I like how MetaMath brags about how easy it is to verify proof by yourself if you're not a mathematician, in the end I don't think it's useful for any people but math-oriented in the first place. It's not going to explain the meaning behind the math (it actually intends to take rid of the meaning) and certainly not solve daily problems like antenna design or machine learning. I rather see it like a collection of theorems declared true by a computer following dumbly (I mean that in a positive sense) a substitution rule and base axioms. It's another kind of beauty.