There is still some confusion here. I'd separate Metamath as a language (implementations, proof assistants, UI) vs. formalization (database, taxonomy, conventions). Clearly their philosophy and goals should be different.
-- You received this message because you are subscribed to the Google Groups "Metamath" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/63b76366-ac60-4dda-ab83-fb7b984c06d1%40googlegroups.com.
