On January 3, 2020 7:12:23 PM PST, Norman Megill <[email protected]> wrote:
The Wikiproofs site (wikiproofs.org) seems to be down
The content is at https://github.com/jkingdon/wikiproofs along with a
few notes about the tools which were used.
, but looking it
up on
archive.org it uses theorem labels like
"introduceBiconditionalFromImplicationsInConsequent". Personally I
think
that would slow me down and I would dislike it. IIRC Jim Kingdon
contributed to that project, and it would be interesting to hear his
experience with long labels.
I guess on the whole it feels pretty similar to set.mm for me.
"InConsequent" was consistently used the way metamath uses a trailing
"d". "detach" was in many theorem names and corresponds to "mp" found in
similar metamath theorems, etc.
I think there was a whole "introduce"/"eliminate" naming convention
which corresponds to many texts (see for example sections A.2.4, A.2.5,
A.2.6, and following sections in the HoTT book), but I don't remember
how well developed that was.
I wouldn't get super hung-up on abbreviations versus whole words. I
think the latter do provide for an easier on-ramp in the early stages.
The former are faster to type (especially if we assume limited/no
autocomplete tools), and do provide a certain conciseness.
More important than abbreviations versus words, I think, is how
consistently the conventions are followed and how natural they feel.
Metamath has made a lot of improvements in this area and at least for me
the difference between "expd" and "exp3a" (or whatever it used to be
called, I forget already) is like night and day. I hope we continue to
improve our names. We haven't reached perfection yet but a spirit of
slow but steady improvement is what has gotten us as far as we have gotten.
I feel like I should conclude by summing up the wikiproofs experience. I
suppose the capsule summary (for wikiproofs and also ghilbert) is that
it is hard for a new system - even one which is compatible or partly
compatible - to get off the ground. But I hope people keep trying. Not
because there is anything wrong with metamath . After all, after trying
to learn/create a whole bunch of provers, metamath is the one which has
so far stuck with me. But because there are still things to work on,
whether it is making it easier to write proofs, easier to browse/read
them (already a big strength of metamath over most others I've seen),
easier to handle very large proof databases (set.mm is a tiny fraction
of known mathematics), easier for people to contrbute proofs, or
whatever other area(s). I'm pretty sure that one or more will eventually
succeed, whether metamath zero, or milpgame, or something else out
there, or something which doesn't even exist yet.
--
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/bfc5f766-e463-0eca-e2e8-77a99f598f7a%40panix.com.
