I am somewhat a type theory partisan, but I appreciate Metamath leading the way, especially on the social side of things. (I would say it is technically primiti

I am somewhat a type theory partisan, but I appreciate Metamath leading the way, especially on the social side of things. (I would say it is technically primitive, but socially advanced, as opposed to say Coq which is more technically advanced but has a very poor track record of fostering wide-scale many-person projects.) Best of luck! The importance is not there is one way that wins out (that would be bad) but that each project seeks to be all-encompassing. We want many maps over all the land, not divvying up the land into unoverlapping fiefdoms, or forcing everyone to be in one big fiefdom.