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]. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/160ba6d7-9342-4f42-8069-9ac2f41b47c1%40googlegroups.com.
