Why would proof shortening be useful?

[Marnix Klooster]

Hello all,

Occasionally I see people here spending effort on making Metamath proofs as short as possible.  And every time I wonder, Why?

Of course it can be a nice challenge occasionally, but I thought proofs were intended to communicate?  So they have a certain structure that can convey some kind of understanding to the reader.

And most shortened proofs, especially the auto-shortened ones, will lack that-- they will only be correct.

I mean, minimizing the number of dependencies, or avoiding specific dependencies, I can understand as a useful goal.  But why would we spend significant effort on shortening proofs?

Thanks!

Groetjes,

 <><

Marnix
--

Marnix Klooster
marnix....@gmail.com

[Norman Megill]

People will probably have different answers, but from my own perspective:

1. Simple shortenings with 'minimize_with' almost always make the proof cleaner and more readable by eliminating redundant bicomd's etc. that happen when the proof is written "sloppily" to save time (as I tend to do).

2. When others find a significantly shorter proof of something I've done, I'm almost always impressed by it and don't recall ever feeling that my original proof was better.

3. With OpenAI-shortened proofs, I guess time will tell, but to pick a random example, compare
http://us2.metamath.org/mpeuni/2exp6.html
http://us2.metamath.org/mpeuni/2exp6OLD.html
The OpenAI proof seems much easier to read. And quicker to read because there are fewer steps.

4. File size savings incrementally improve everyone's experience by reducing editor load time, verification time, disk space, web page load time, etc. Over many users that adds up.

Overall, it has been rare (if ever) that I have considered longer proofs easier to read. Maybe there will be some OpenAI case where the shorter proof is really cryptic and hard to understand; if so, that in itself would be interesting to me because I don't think it happens often.  It might even suggest a useful new proof technique.

Finally, there is the question of what Metamath proofs are for. Communicating to humans is only part of their purpose, supplementing and filling in gaps in literature proofs; for me, the assurance that computer-verified correctness provides is just as important if not more so. Making the verification process as quick as possible seems like a good thing, and shorter proofs are part of that.

Norm

[Richard Penner]

On Friday, March 27, 2020 at 11:25:25 AM UTC-7, Marnix Klooster wrote:

Hello all,

Occasionally I see people here spending effort on making Metamath proofs as short as possible.  And every time I wonder, Why?

From one point of view, "I just want to know what the theorems say" the shortness of the proof means little. But for the business of collecting a large number of proofs, having shorter proofs is a boon to those that have to store them, read them and understand them. Indeed, most proofs in the database can be expanded to thousands of steps by eliminating their dependence on proofs that came before, so emphasis on shortening proofs is practical even from the non-mathematical viewpoint of a curator.

Shortening a proof means either a) one has eliminated wasteful steps by taking a more direct route, avoiding deriving the same statement twice, or using a step like "bicomi" (commuting a logical equivalence) more often than required or b) it means you proved the same statement with more powerful tools. And powerful tools are good things.

Since Metamath builds up from the axioms, it starts a long way from the concepts that even children using math deal with on a daily basis ("2p2e4" is an example, since this concept of addition is powerful enough to work on negative, rational and complex numbers while the underlying set theory pieces don't speak immediately to such concepts).

A recent example would be "intss" (If A is a subclass of B, then the intersection of class B is a subclass of the intersection of class A) which was shortened from a 10-step technical argument about the elements of A and B to a 5-step proof which points out that the subset relation of A and B gives rise to an implication of restricted quantifications, which gives rise to a subclass relation between classes of element which meet those restricted quantifications. When those classes are equated with the definition of the intersection of a class, we are done.

The shorter proof is easier to translate. It's more symmetric in that it treats A and B identically. It's philosophically more concise in that it doesn't rely on the existence of a universal class of all sets.

References:

http://us.metamath.org/mpeuni/bicomi.html (logical equivalence commutes)

http://us.metamath.org/mpeuni/2p2e4.html ( 2 + 2 = 4 )

http://us2.metamath.org:88/mpeuni/intssOLD.html (short lived link to proof from 1999)

http://us2.metamath.org:88/mpeuni/intss.html (short lived link to proof from 2020)

[Mario Carneiro]

I think the other posters have covered my thoughts on the matter already, so I won't add much, but I did want to mention that regarding machine learning to generate short proofs, I think it is extremely unlikely that the proofs that are generated are going to be harder to understand than the originals. The reason is because machine learning "thinks like a human" in a number of respects; it learns heuristics and styles just like we do, even when these heuristics are not absolutely optimal. You are much more likely to find "bad short proofs" through exhaustive search or hard optimality constraints, such as dfbi1gb.

Mario

--
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/bb9250a2-60fc-45e2-bc37-1520bd6d60a7%40googlegroups.com.

[Benoit]

I agree with the previous answers (Mario meant dfbi1ALT instead of dfbi1gb -- its label has been changed recently to conform to conventions).

I'll add that indeed, shorter metamath-proofs are very often easier to read and understand.  When this is not the case, or when there are several genuinely different proofs, then it is a good idea to keep both (or more) proofs by using the xxxALT convention, as in dfbi1ALT.

Benoît

To unsubscribe from this group and stop receiving emails from it, send an email to meta...@googlegroups.com.

[Dirk-Anton Broersen]

He Marnix,

 

(It’s an interessting idea you have. Like if a short proof is interessting.

 

The thing is where a proof is a result. It’s build up with different sightings and if formula (‘s).

 

Formula’s can be discussed where a proof is like undenieable.

 

 

For instance, A + B = C or A + A = B then A + B = 3A hence C = 3A; only if A + A = B. So 2A = B then 3A = C if A + B = C but A + B = C is true; even if not A + A = B.

 

 

A proof is A² + B² = C²; because of the greek law. You can draw it with lines in this consensus. Line 90 degrees line connected with a line (straight lines).

 

The proof is that the areal surface of A² + the areal surface of B² = the areal surface of C²

 

This one you can draw out according to the Greek law.)

 

 

Having sayd this long proofs and short proofs are likely understoot by mathematicians so..

 

 

With friendly regards,

 

Dirk-Anton Broersen

 

 

Verzonden vanuit Mail voor Windows 10

--

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/CAF7V2P-KT1S23_whnDhgFE0HoW%3DdQkOxcyLm0DoM%2B-vkf9sepA%40mail.gmail.com.

 

[ookami]

> Occasionally I see people here spending effort on making Metamath proofs as short as possible.  And every time I wonder, Why?

Because it is fun.

Because it helps me understand the overall structure of a topic better, when I do proofs myself.

Because usually not only a particular proof becomes more readable, but surrounding proofs

as well. This is because a shortening is sometimes possible only, when proofs are reordered.

In effect, theorems become layered, the more basic ones bubbling up to early positions.

This rearrangement is in itself helpful for understanding.

Another sort of refactoring effect is visible when common subproofs are singled out into lemmas.

Again, this has a positive effect on readability.

This is not the ordinary case, but I have cut down several proofs roughly into half,

sometimes even less, starting from 50 essential steps or so. The result is way more readable

than the origin, I believe.

Wolf Lammen