On Friday, June 14, 2019 at 4:06:03 PM UTC+2, Alexander van der Vekens wrote: > > Why is the theorem ~ 4syl discouraged? The comment says: > > The use of this theorem is marked "discouraged" because it can cause the >> "minimize" command to have very long run times. However, feel free to use >> "minimize 4syl /override" if you wish. Remember to update the Travis >> "discouraged" file if it gets used. >> > > Actually, there are 191 uses of "4syl" in set.mm! So is there (still) a > relevant impact on "minimize" or another reason why it is discouraged? >
The reason is still the same: launch a "> minimize 4syl" on a long proof, and it will take a very long time. As Norm told me when I proposed to add 4syl, the "minimize" algorithm has something like exponential time complexity in the number of $e-hypotheses of the theorem to minimize with, and 4syl has four $e-hypotheses... I agree that it is a useful theorem, but you can see manually if it is worth to launch a "minimize 4syl/override": if your proof already uses 3syl and chains it with a syl, for instance. Benoit -- 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/3f33e139-b7e3-49b9-bef2-d5a36e5a357d%40googlegroups.com.
