To be honest, I feel it quite inappropriate to post this page, inasmuch as anyone reading this post probably - bar an errant search - shouldn't be editing that page.
On Sunday, July 7, 2019 at 11:13:36 PM UTC-4, Norman Megill wrote: > > 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/52825472-f500-4a9f-a3d2-a04de4432e99%40googlegroups.com.
