On Wednesday, February 12, 2020 at 5:53:59 AM UTC-5, Alexander van der Vekens wrote: > > On Wednesday, February 12, 2020 at 10:00:42 AM UTC+1, David Starner wrote: >> >> There might be an error in the minimize command; it found that axdc >> has a much shorter proof using ax-dc, which is obviously true yet >> defeats the purpose of the axdc theorem ( >> http://us.metamath.org/mpegif/axdc.html ) and uses new axioms for that >> theorem. >> >> I think ~axdc must be tagged with "(Proof modification is discouraged.)", > so that minimize will not touch its proof. This is not an error of the > minimize command. >
David is right, there is something very wrong here. While ~axdc should be tagged with "(Proof modification is discouraged.)" but isn't, in any case 'minimize' should not be bringing in the new axiom ~ax-dc. We should hold off on any more runs until I determine what is happening and fix the program. Based on what I find, the jobs may have to be restarted. Thanks, David, this was a good observation. Norm -- 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/d238ecbe-0ba0-4d6e-b164-7d1bbca42c88%40googlegroups.com.
