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<https://go.microsoft.com/fwlink/?LinkId=550986> voor Windows 10 Van: Marnix Klooster<mailto:[email protected]> Verzonden: vrijdag 27 maart 2020 19:25 Aan: Metamath<mailto:[email protected]> Onderwerp: [Metamath] Why would proof shortening be useful? 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 [email protected]<mailto:[email protected]> -- 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/CAF7V2P-KT1S23_whnDhgFE0HoW%3DdQkOxcyLm0DoM%2B-vkf9sepA%40mail.gmail.com<https://groups.google.com/d/msgid/metamath/CAF7V2P-KT1S23_whnDhgFE0HoW%3DdQkOxcyLm0DoM%2B-vkf9sepA%40mail.gmail.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/HE1P189MB0282E3FBB85EEDE60EC771F283CC0%40HE1P189MB0282.EURP189.PROD.OUTLOOK.COM.
