Problem with us2 ?

[Benoit]

Hi,
If I recall correctly, the us2 server is updated within 24 hours of a new merge in metamath/set.mm on github (I cannot retrieve this information).  But the merge https://github.com/metamath/set.mm/pull/1261#event-2813593206 is from 20 nov. 2019 à 02:26 UTC+1 (33 hours ago at the time of writing this message) and still does not appear in http://us2.metamath.org/ileuni/mmrecent.html (which indicates "Last updated on 19-Nov-2019 at 8:14 PM ET").  Is there a synchronization issue ?
Thanks,
Benoît

[ookami]

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

[Jim Kingdon]

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

[Norman Megill]

Sorry, I encountered a problem testing a metamath.exe modification, so I abandoned the site build.  The site is updated now.

In general I do try to rebuild the site within 24 hours of a PR but occasionally there may be a delay.

Norm

[Norman Megill]

No, it had nothing to do with your PRs.  I am greatly appreciative of the work you are doing.

Norm

[ookami]

Am Donnerstag, 21. November 2019 16:38:57 UTC+1 schrieb Jim Kingdon:

...

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).

I'd love to look into all the different aspects of logic.  Unfortunately, I work full-time in a completely different area, and I have simply no time to follow all the different threads.  I do not even have time to become specialized in the fields I really want to know.  So don't expect too much.

Wolf

[David A. Wheeler]

On Thursday, November 21, 2019 at 7:52:51 AM UTC-5, ookami wrote:
>>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.

On November 21, 2019 12:13:50 PM EST, Norman Megill <n...@alum.mit.edu> wrote:
>... I am greatly appreciative of

>the work you are doing.

Me too.

Simpler proofs are always nice, but there's also another reason I'm interested. I expect that in the future there will be many efforts to develop automated provers based on machine learning. Improved training material should help any machine learning system. So please carry on!!

--- David A.Wheeler

[Benoit]

A word of caution (without being dismissive whatsoever of Wolf's great work): shorter proof (or, more precisely, proof with fewer steps) does not always mean simpler proof, or easier-to-understand proof.  This is why I am thankful that Wolf keeps *OLD versions (which should be checked before being deleted), and whenever the older proof has any interesting feature, it should be kept as *ALT (or *ALT2, etc.).  This may be the case (this is not automatic) when:
- the longer proof (for the number of steps), actually has fewer essential steps (I have seen a few cases, which unfortunately I do not remember),
- there is a tie, either in the number of steps or of essential steps,
- there exists a proof with fewer steps using more axioms (in which case it is this one which should be the *ALT),
- the longer proof uses fewer definitions, or fewer syntax definitions (more precisely: there exists a definition used by the shorter proof which is not used by the longer proof),
- any other interesting feature, which makes the longer proof more understandable, or have more structure, etc. (this part is obviously more subjective).

I lean to the side of having more alternate proofs rather than possibly losing some information which might appear useful only in the future.  I also note that in the case of machine learning, having more alternate proofs may also be an advantage.

Benoît

[ookami]

The rules by which a proof is considered shorter were explained to me by Norm about 10 years ago: First look at the size of the encoding of the compressed proof, not taking the references into account. On tie, count the number of symbols used in the HTML display of the proof. I used the second rule extremely seldom in the past years, maybe twice or so. And I extended these rules by allowing one proof to be longer, if another/others benefit such, that in total their combined proof size shrinks. A recent example of this is neneqad. eqcom is an example that uses more definitions than the OLD one, and eqeq12i has the essential steps increased. All of these cases combined are rare, fewer than 5% I guess out of hand. Are shorter proofs less readable than others? IMO, certain techniques making twisted use of negation (like nsyl) force me occasionally to look/think twice. So, yes, from my personal perspective... it can happen.  But not being able to grasp negated formulas that easily I consider my personal disadvantage.  This is not really an objective argument  As for the avoidance of definitions... well, what are they meant for, then? Is it really a good idea to expand them? And to take the idea further, theorems are again obstacles on the way to simplify proofs to just a sequence of axioms. I cannot quite follow here. But please, see and decide yourself whether the results mandate a change of rules. I gave you the examples above

Wolf

[Benoit]

On Thursday, November 28, 2019 at 2:18:19 PM UTC+1, ookami wrote:

The rules by which a proof is considered shorter were explained to me by Norm about 10 years ago: First look at the size of the encoding of the compressed proof, not taking the references into account. On tie, count the number of symbols used in the HTML display of the proof.

We all agree with this, and nothing in my previous post contradicts this.
 

I used the second rule extremely seldom in the past years, maybe twice or so. And I extended these rules by allowing one proof to be longer, if another/others benefit such, that in total their combined proof size shrinks. A recent example of this is neneqad. eqcom is an example that uses more definitions than the OLD one, and eqeq12i has the essential steps increased. All of these cases combined are rare, fewer than 5% I guess out of hand.

Applying what I proposed in my previous post, eqeq12iOLD should be relabeled eqeq12iALT (with both discouragement tags), its comment could read "Alternate proof of ~ eqeq12i , longer but with fewer essential steps" and the comment of eqeq12i could mention "See also ~ eqeq12iALT for a longer proof, but with fewer essential steps."

As for eqcom, I think that eqcomOLD can be deleted (referring to the part of my previous post where I wrote "this [keeping the longer proof as ALT] is not automatic").

As for neneqad: I would keep neneqadOLD and relabel it neneqadALT (since, as I wrote in my previous post, "I lean to the side...") but I admit that here, this is debatable.

Are shorter proofs less readable than others?

No, they need not be, and most of the times, they are not.  As I wrote in my previous post, "shorter proof does not always mean easier-to-understand proof".  Not the same thing.
 

IMO, certain techniques making twisted use of negation (like nsyl) force me occasionally to look/think twice. So, yes, from my personal perspective... it can happen.  But not being able to grasp negated formulas that easily I consider my personal disadvantage.  This is not really an objective argument  As for the avoidance of definitions... well, what are they meant for, then? Is it really a good idea to expand them?

I did not suggest this.  What I meant is that if a "naturally obtained" proof turns out to use fewer definitions, then it may be the case (as I wrote in my previous post, "this is not automatic") that this proof has an interesting feature which might make us want to keep it as an ALT proof.
 

And to take the idea further, theorems are again obstacles on the way to simplify proofs to just a sequence of axioms. I cannot quite follow here. But please, see and decide yourself whether the results mandate a change of rules. I gave you the examples above

The rules neet not be changed.  As before, if the proof you obtain is shorter (according to the rules that you stated), then this should be the main proof.  What I meant to say is: the older proof may sometimes be worth keeping as an ALT proof, because of this or that special feature.

Benoît

[Jim Kingdon]

On 11/27/19 10:10 PM, 'ookami' via Metamath wrote:

> I'd love to look into all the different aspects of logic.  Unfortunately, I work full-time in a completely different area, and I have simply no time to follow all the different threads.  I do not even have time to become specialized in the fields I really want to know.  So don't expect too much.

No worries, I'm not assigning homework to you or anyone else.

Just a statement about some of what is out there in case it catches anyone's fancy.

[Alexander van der Vekens]

I think there is no contradiction in the approaches of Wolf and Benoît: Wolf is talking about the main proofs, and Benoît about alternate proofs, providing criteria to keep (ALT) or to delete (OLD) theorems with different proofs. Therefore, both opinons are valid. A good, additional example is my theorem cayleyhamilton, which I provided with two proofs: the main one using ($e statement) definitions, and an ALT variant which does not use these definitions, but expand them, resulting in longer lines in the proof (for details see https://groups.google.com/d/msg/metamath/-RLnH6BcNTo/_kIagCsqAgAJ).