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 On Friday, March 27, 2020 at 2:25:25 PM UTC-4, 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? > > 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 > -- 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/15bbdc30-63e6-4847-81c7-43da12b74aaa%40googlegroups.com.
