Also concerning axioms dependency I presume there is a tension between proof length and axiom dependency size that is probably more prevalent for low level theorems and much less important for higher level theorems where proof length is probably the only thing that matters?
Is there any consensus on that? -stan On Thu, Mar 26, 2020 at 6:01 PM Stanislas Polu <[email protected]> wrote: > Thanks Benoit, > > Great points. Is there a metamath-exe way to compute the axioms dependency > so that I can run that analysis? > > Concerning keeping an OLD version, happy to do so. I’ll update the PR > accordingly unless I hear otherwise. > > I’ll prepare a summary of our approach to share with the community as well. > > Best, > > -stan > > On Thu, Mar 26, 2020 at 5:54 PM Benoit <[email protected]> wrote: > >> That's very interesting and promising ! >> >> Did you make sure that no new axiom dependencies were introduced in the >> proofs ? Is it possible to keep the older proofs as "xxxOLD" with the >> comment "Old proof of ~ xxx . Obsolete as of 26-Mar-2020. " and both >> discouragement tags ? This would ease comparisons and might give some >> insight on the kind of shortening introduced. >> >> Is it possible to have some details on the model that you used ? >> >> Benoît >> >> -- >> 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/833aa5a4-23f0-4a30-bbaf-b49acaa3a510%40googlegroups.com >> <https://groups.google.com/d/msgid/metamath/833aa5a4-23f0-4a30-bbaf-b49acaa3a510%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 [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/CACZd_0yWZPj0_Eudmw6MU4AJWbiUTewtX0uCf4yJBxET2voajQ%40mail.gmail.com.
