Good point about the conflict of interest (there is lots more detail at
https://en.wikipedia.org/wiki/Wikipedia:Plain_and_simple_conflict_of_interest_guide
- one interesting suggestion of which is that posting to the Talk page
of the article is a lot more kosher than editing the article itself - in
a case like this where the article is about yourself or your organization).
The screen shot, in addition to picking a better theorem than the april
fool's one ("tacky" might be fair, but "not very illustrative of what is
really in set.m" is sort of maybe the way I'd say it), should look
better (which is probably just be a matter of screenshotting a mpeuni
rather than mpegif page).
There is a fair bit of just general updating which would be nice, that's
probably the #1 thing which stands out. I did just fix one out-of-date
statement about what set.mm covers, but there's more of this sort of thing.
On 7/7/19 8:13 PM, 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]
<mailto:[email protected]>.
To view this discussion on the web visit
https://groups.google.com/d/msgid/metamath/3c546632-f6a2-434c-a3d5-29a2baba8e71%40googlegroups.com
<https://groups.google.com/d/msgid/metamath/3c546632-f6a2-434c-a3d5-29a2baba8e71%40googlegroups.com?utm_medium=email&utm_source=footer>.
--
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/63e598fa-9175-7c5e-9bbd-73e9d2e0cfcc%40panix.com.
