Minimized footex #3269
Minimized footex #3269
Conversation
|
perhaps it's the |
|
Thank you for dedicating time and computing power for this! I don't know exactly how the minimizer works so these are wild guesses, but it could be the length (and complexity) of the steps statements. It might also be the high number of hypotheses used in Geometry, but then other geometry and algebra theorems should have the same issue. |
|
@GinoGiotto - I applaud your perseverence! I have no idea why it's so hard to minimize this case. |
|
@tirix One thing that I would recommend for this proof, just as a general readability thing which may help with the minimize (based only on pure speculation) is to split the core of the proof out into a lemma, basically once all the assumptions have been established and you are working within some local context. See for example pnt3, which calls pntleml after adding a bunch of hypotheses, which calls pntlemp after adding hypotheses, which calls pntleme after adding even more hypotheses. Doing this keeps the statements somewhat readable by hiding the context behind the variable |
|
I opened an issue here #3271 to discuss this more thoroughly. |
I think minimizing flt4lem5e is prohibitively long because, despite only being 27 lines long, there are 71 Zs, so there are 46140 steps when expanded+syntax. (Relevant: metamath#3269) I used theorems in Scott's mathbox without even realizing, so they're moved now I renamed dvdspw to reduce confusion with dvdsexp Fix comment of ncoprmgcdne1bgd
I managed to minimize footex, the only theorem that I had to skip in my recent global minimization process, due to the excessively long time it demanded.
Footex is a nasty theorem, even basic commands like
prove footexorshow proof footex /compressedare time-challenging. I believe it needs revision because I find it to be impractical to work with (ping @tirix since he contributed it).The first time I attempted to minimize it, I used metamath-exe
version 0.198, and as stated in #3180, the program crashed. This time I usedversion 0.199.preand successfully got this PR as a result. I didn't replicate these observations, so I'm not sure if it's actually the new version that made the difference.A note that I find interesting:
footexhas neither the longest proof nor highest number of steps in main, despite this it takes days to minimize, which is by far the longest duration I encountered in my global minimization activity. For comparison, the most challenging theorems need at most some hours to minimize, not even close to the time required byfootex.Since the proof of
footexisn't that long, it seems to me that proof length isn't the only factor that matters to determine the execution time to shorten it. So I believe that the addition of a/SKIPLONGPROOFoption proposed in metamath/metamath-exe#95 might not be the most effective solution for avoiding such significant time requirements, and I agree with the recent decision to close it.I still wonder tho, why is
footexso bad? Perhaps it's related to the presence of numerous distinct variable conditions? I really don't know, but I believe it would be interesting to get a better undertanding of it in order to avoid such time-draining theorems in the future.