On Mon, Feb 12, 2024 at 8:40 AM Glauco <glaformetam...@gmail.com> wrote:
> The proofs produced by mmj2 are not exactly the same, because (in my > opinion) mmj2 has a small bug in the knapsack algorithm > > IMHO, metamath.exe and mmj2 don't produce the same compressed proofs (I've > shown several examples, in the past) > I would be interested to hear specifics about these claims, because they are supposed to be the same and I haven't heard any bug reports to the contrary. I also don't understand what knapsack bug you are describing or why it is a matter of opinion whether it is a bug. > > > -- > 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 metamath+unsubscr...@googlegroups.com. > To view this discussion on the web visit > https://groups.google.com/d/msgid/metamath/f687d4b6-412f-4be0-92b8-4d92dd893277n%40googlegroups.com > <https://groups.google.com/d/msgid/metamath/f687d4b6-412f-4be0-92b8-4d92dd893277n%40googlegroups.com?utm_medium=email&utm_source=footer> > . > -- 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 metamath+unsubscr...@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/CAFXXJSuKbEWmMbEsfd_A%2BcCXxCVRVExdKxv8hwVgTnBhRQBhow%40mail.gmail.com.
