I will give my opinion on what should be in the wikipedia article. Mainly two issues: a) the operating principles of metamath. b) In which cases it can be used and in which cases it cannot be used.
>From that point on, it seems to me that this is the right blueprint: 1) operating principles. The substitution algorithm used by metamath. The peculiar provisos of metamath. 2) Comparison with other provers. Logic plugged into the software vs simple verification of substitutions. Provers using a typed lambda calculus vs provers using FOL + ZFC. Possibility to use any logic in metamath. Only restriction: it's not suitable for Gentzen style. 3) Tools: mainly mmj2 in the O'cat version. Carneiro's is not yet ready. Except for the algorithm checking that the system is sound. Using metamath yourself to enter a proof is not recommended: there is no good syntactic interpreter. 4) Databases. Anything you want by indicating the limits of use of each. The database on the New Foundation. It is correctly commented and there are textual references. The intuitionism database seems to have some interesting comments on the entry page and on the axioms but then it's much more succinct. 5) When to use metamath? For all kinds of logics: classical, intuitionist, modal, lambda calculus typed or not. For set theory. Metamath is relatively well adapted for structures (algebraic, topological) and for everything that resembles structures: geometry (Euclid's or Tarski's), graph theory, category theory. On the other hand, metamath is completely unsuitable for concrete calculations. If you have to do multiplication, choose another checker. Metalogics is not so good either. And algorithmic studies must be a little cumbersome. But it remains to be confirmed. 6) Do not use metamath below the baccalaureate. Voilà: it seems to me that this should make a correct page. -- FL -- 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/c1c5bc89-9d36-416f-9792-90488d77b986%40googlegroups.com.
