No, it had nothing to do with your PRs. I am greatly appreciative of the work you are doing.
Norm On Thursday, November 21, 2019 at 7:52:51 AM UTC-5, ookami 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 is doing lots of 'homework'. So generally, I simply prove each and > any theorem on my own, without noticing the current proof. When 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 an 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/9d1265c0-7e51-45d5-95b9-7cdd5a608cf7%40googlegroups.com.
