The content of https://en.wikipedia.org/wiki/Metamath is somewhat outdated and doesn't reflect the current focus. Since I am mentioned several times on the page, I have chosen not to edit it myself because it would feel like a conflict of interest. But anyone else is welcome to update it.
Suggestions: 1. The Hilbert Space Explorer and Quantum Logic Explorer shouldn't be mentioned at all. 2. The "explorers" for iset.mm, nf.mm, hol.mm are much more important but aren't mentioned. 3. Using the April Fool joke theorem as an example seems tacky. 4. That Metamath holds a prominent place on Freek's 100 theorem list might be useful to mention. 5. The description of 3rd party verifiers, proof assistants, and IDEs could be updated. Feel free to add other suggestions here. Feel free to edit (and hopefully improve) the page at your convenience. The pages for other provers such as Mizar, HOL Light, Coq, Isabelle, etc. might offer ideas. However, they are sometimes shorter than Metamath's, and there doesn't seem to be consistency in the length, style, or level of detail. So in the end you have to use your own judgment. Thanks, Norm -- 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/3c546632-f6a2-434c-a3d5-29a2baba8e71%40googlegroups.com.
