This is great stuff. Both in terms of the improvements to set.mm but
also the example of how it can be a learning tool (which it also has
been for me).
I'll also say that if you have any interest in, or curiosity about,
intuitionistic logic, that there is low hanging fruit in iset.mm. Proofs
that can be shortened, cases where set.mm has a better proof which can
be copied over, probably some cases where iset.mm has a shorter proof
which can go over to set.mm.
The work is (usually) quite similar to set.mm (a fair number of proofs
can be copied over unmodified, for example) and there is a detailed "how
to" guide at http://us.metamath.org/ileuni/mmil.html#intuitionize
(suggestions on making the web pages and comments clearer are also welcome).
On 11/21/19 4:52 AM, 'ookami' via Metamath wrote:
I am not sure whether my recent shortenings, a flurry of more or less
trivial "improvements", is responsible for the observed behaviour. As
a side effect, these small changes push back other more significant
contributions on the recent changes page. I am fine with the current
proceeding, but I feel I should explain why I take this smaller proof
challenge so serious.
I have no education in logic, let alone formal logic, so becoming
familiar with a new field means climbing a steep learning curve for
me. One way to succeed in doing so is doing lots of 'homework'. So
generally, I simply prove each and any theorem on my own, without
noticing the current proof. If I compare my result to that of 'prior
art', and there is a difference, I either improve my technique, or
submit a shortening pull request.
There is some merits to this idea, perhaps not so obvious: The overall
structure of a section improves, because important/central theorems
slowly bubble up to the front, and duplicated proofs are avoided. And
among a lot of trivial changes there are some jewels, where a
unnecessary complicated proof becomes simple.
Wolf
--
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/160ba6d7-9342-4f42-8069-9ac2f41b47c1%40googlegroups.com
<https://groups.google.com/d/msgid/metamath/160ba6d7-9342-4f42-8069-9ac2f41b47c1%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/8ae1e185-5093-0da5-9ee9-e1167bd9c00e%40panix.com.
