Uhmm, well length^2 is difficult where 1 x 3V2 x 3V2 x 3V2 = 2 ; in the mid-section (3V2)^2. ( a Multi-plecation of the “length” where the cube doubles)
1+ 0,25992104989487316476721060727823 (=3V2) + 0,32748000207332630998449503199408 + 0,41259894803180052524829436072769 =2 Length ^2 = squared surface area. Hence Length ^2 = not another length. In fact it is. Increasing and decreasing (shortening) are thesame like +1 or -1. Maybe I don’t really get the point, With friendly regards, Dirk-Anton Broersen Verzonden vanuit Mail<https://go.microsoft.com/fwlink/?LinkId=550986> voor Windows 10 Van: 'Stanislas Polu' via Metamath<mailto:[email protected]> Verzonden: donderdag 26 maart 2020 18:03 Aan: [email protected]<mailto:[email protected]> Onderwerp: Re: [Metamath] Re: Deep Learning powered proof shortening 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]<mailto:[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]<mailto:[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]<mailto:[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]<mailto:[email protected]>. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/CACZd_0yWZPj0_Eudmw6MU4AJWbiUTewtX0uCf4yJBxET2voajQ%40mail.gmail.com<https://groups.google.com/d/msgid/metamath/CACZd_0yWZPj0_Eudmw6MU4AJWbiUTewtX0uCf4yJBxET2voajQ%40mail.gmail.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/AM0P189MB0722D4C591A622EFCE19166883CF0%40AM0P189MB0722.EURP189.PROD.OUTLOOK.COM.
