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