Fun with metamath.

Written 20.06.2018

While reading wikipedia on different subjects in proof calculus I found link to metamath. Metamath is similiar to site I was thinking writting here. Problem I have with metamath is that eventhough it explains good detail what are it's axioms and what axioms are added when more subject are taken in it really doesn't explain why. It references Tarski's axioms but it doesn't note that major thing about these axioms is that they are tautologies. That simple thing already makes axioms much more understandadble. Other example where lack of this example is annoying is when you try to open definition of complex limit you end up this $Slot9$ which simple wikipedia search I didn't find anything understandable. Maybe I could understand if I had studied more topology but should I need to or should metamath have better explanation ready? Anyhow I really would like to find some bit more complex on metamath and open it fully but I think I have to learn more on certain topics before I could do that.