Wow, thank you very much! Just FYI, in the 20190602 version of the Metamath book, in the "write source" subsection (5.3.2) there is no option for /extract. On Saturday, April 6, 2024 at 6:45:50 PM UTC+2 [email protected] wrote:
> > Now I want to create this set_simplified.mm file. Mario Carneiro > suggests to use a ""metamath aware" slicer". Is there such a slicer already > created? > > Yes, there is already such slicer, you do the following: > > READ set.mm > WRITE SOURCE 2p2e4.mm /EXTRACT 2p2e4 > > This creates a working .mm file that contains only the 619 theorems needed > for 2p2e4, the necessary axioms, and the other technical stuff (latex > definitions, variables, constants ecc..). > > Il Sab 6 Apr 2024, 00:56 Anarcocap-socdem <[email protected]> ha > scritto: > >> Thank you for all the answers, they are quite informative. >> >> Now I want to create this set_simplified.mm file. Mario Carneiro >> suggests to use a ""metamath aware" slicer". Is there such a slicer already >> created? I guess it is not as easy as just deleting, from set.mm, the >> subtheorems that are not needed for 2p2e4. I guess that quite a few other >> steps need to be taken in order to ensure the set_simplified.mm works >> properly. >> >> Could somebody give me a hand on this project? >> >> Thanks! >> > >> On Wednesday, April 3, 2024 at 1:15:41 AM UTC+2 [email protected] wrote: >> >>> On Tue, Apr 2, 2024 at 6:56 PM Anarcocap-socdem <[email protected]> >>> wrote: >>> >>>> Thank you very much for the answer. >>>> >>>> Let us see if I understand this: >>>> >>>> Let us assume I take the 619 different subtheorems used in 2p2e4 (I get >>>> this number, 619, by doing SHOW TRACE_BACK 2p2e4 /COUNT_STEPS). These 619 >>>> subtheorems can be listed by doing show trace_back 2p2e4. The total number >>>> of steps of these 619 subtheorems is 12178 (again, this number is obtained >>>> by doing SHOW TRACE_BACK 2p2e4 /COUNT_STEPS). >>>> >>>> So, is it correct to say the following: >>>> >>>> - I can create a new file, let us call it set_simplified.mm, which >>>> corresponds to taking set.mm, and only keeping the 619 subtheorems >>>> used in the proof of 2p2e4. >>>> - I can run python3 mmverify.py set_simplified.mm --logfile set.log to >>>> check that the proof is correct. mmverify.py has about 690 lines. >>>> >>>> So, with 12178 steps, plus 690 lines, I can get a full proof of 2p2e4. >>>> All these steps could be written in a pdf file (long, but not unreasonably >>>> long). >>>> >>>> Is this correct? Or maybe the way I have defined set_simplified.mm is >>>> "too simplified"? >>>> >>> >>> Yes, that is basically correct. Strictly speaking though it is "too >>> simplified", because it doesn't account for statement types other than $p / >>> $a : >>> >>> * ${ , $} - obviously we need these for grouping a statement with its >>> hypotheses >>> * $e - (hypotheses) these are "attached" to each theorem and usually >>> directly precede them, although sometimes they can be in the same scope as >>> an earlier theorem and shared across multiple theorems >>> * $d - (disjoint variable conditions) these are also hypothesis-like in >>> their scoping pattern and semantics >>> * $v, $f - (variable declarations) for set.mm these are basically >>> global, but there is still a well defined notion of "use" of a variable: >>> just look for its token in any of the 619 subtheorems. If you see it then >>> it must be declared, otherwise it can be dropped. >>> * $c - (constant declarations) These are global, and have the same kind >>> of "use" as variables: if you see it in the $p ... $= or $a ... $. text >>> then it must be declared first. >>> >>> For all these reasons, you probably want to use a "metamath aware" >>> slicer for constructing these *_simplified.mm databases. But this is >>> all very straightforward and will not add much on top of the 619 theorems >>> you identified. None of these count as "steps" though toward the 12178 step >>> count; these are for proof steps (I don't know whether syntax steps are >>> included or omitted in the count), and the best you can say about its >>> relation to the simplified.mm file is that every step requires at least >>> one character so set_simplified.mm should be at least 12178 characters >>> and probably more because of theorem statements, delimiters, formatting, >>> and comments if you are keeping them. >>> >>> In general, no this process will not produce long proofs. In fact it's >>> about as short as we know how to make them, since this is taking full >>> advantage of metamath's abstraction and reuse mechanisms, and the library >>> itself is optimized for overall proof size. However you can find some >>> inefficiencies in this process because set.mm is trying to prove more >>> than just 2+2 = 4 so it will prove things in "unnecessary" generality that >>> becomes pure overhead once you cut literally everything else out. So it's >>> likely that after extracting such a database you can run minimizers over >>> the code and get still more savings. >>> >>> >>>> On Monday, April 1, 2024 at 10:48:46 PM UTC+2 [email protected] wrote: >>>> >>>>> > 1. In https://us.metamath.org/mpeuni/mmset.html#trivia, it is >>>>> stated that "A longest path back to an axiom from 2 + 2 = 4 is *184 >>>>> layers* deep". However, if I run show trace_back 2p2e4 /count_steps, >>>>> it is stated that "The maximum path length is 84". Is there a typo >>>>> somewhere? (84 != 184). >>>>> >>>>> Note that that statistic is one of those that will go out of date >>>>> quickly due to changes in the library structure. So you should not expect >>>>> it to be exact, unless we have an automated mechanism for keeping it up >>>>> to >>>>> date, and we don't currently. However, there is one major change between >>>>> when that text was written and now which significantly decreased most of >>>>> the numbers quoted, which is the isolation of the real numbers from their >>>>> construction. 2+2 = 4 is a theorem very close to the axioms of real >>>>> numbers, so it was reduced from something depending on the entire stack >>>>> of >>>>> set theory and the construction, down to just a few direct axiom >>>>> applications (plus still a bunch of set theory because of the use of >>>>> df-ov >>>>> "operation value" for expressing the + function, defined in the set >>>>> theory >>>>> section). >>>>> >>>>> In order to get something closer to the "true" original numbers, you >>>>> should replace "ax-mulcom $a ... $." with ax-mulcom $p ... $= <apply >>>>> axmulcom> $. and similarly for all the other axioms in the same section. >>>>> This will allow metamath-exe to see that uses of these axioms actually >>>>> depend on a big stack of other lemmas when calculating statistics like >>>>> max >>>>> depth and full-expansion theorem counts. >>>>> >>>>> > 2. If I run show trace_back 2p2e4 /count_steps, it is stated that " >>>>> a total of 619 different subtheorems are used. The statement and >>>>> subtheorems have a total of 12178 actual steps (...) The proof would have >>>>> 5887862241803 =~ 5.9 x 10^12 steps if fully expanded back to axiom >>>>> references.". What is the difference between the 12178 steps, and the 5.9 >>>>> x >>>>> 10^12 steps? I guess that 12178 steps refers to the case in which we take >>>>> the axioms of the complex numbers as "axioms", and 5.9 x 10^12 when we >>>>> also >>>>> prove the axioms of the complex numbers, starting from ZFC. But I am not >>>>> 100% sure, and I would like to have confirmation of that. >>>>> >>>>> No, this is not about that. Metamath theorems are able to refer to >>>>> previous theorems multiple times, in multiple concrete instantiations. >>>>> That >>>>> is, a theorem is really a "theorem schema" over the assignments to the >>>>> wff >>>>> and class variables. If you wanted to perform the same proof in pure >>>>> first >>>>> order logic, you would have to redo the proof for every choice of those >>>>> wff >>>>> variables. So the statistic here (also calculated by metamath-exe) is >>>>> working out an approximation to the (exponential) speedup this >>>>> accomplishes, by seeing how many steps would have been taken if you had >>>>> to >>>>> replay each use of each theorem. Effectively, you can think of this as >>>>> treating every metamath theorem as a macro which expands to a proof >>>>> containing more macro references, and if we macro-expand everything all >>>>> that remains are direct references to the axioms. It's easy to get >>>>> exponential growth in this process, since theorem 2 can use theorem 1 >>>>> twice, theorem 3 uses theorem 2 twice and so on. Of course the metamath >>>>> library is not quite so pathological as that, but the nature of the >>>>> process >>>>> is still exponential, where the base is related to the density of >>>>> converging paths in the DAG of theorem references. >>>>> >>>>> > 3. Is there some way to print/export to file the 12178 steps, and >>>>> even the 5.9 x 10^12 steps, all at once? I ask this since running show >>>>> trace_back 2p2e4 /tree gives me a tree, but with only the name of the >>>>> subtheorems, not the steps themselves. And I have been unable to find a >>>>> command that gives the full number of steps, all at the same time. >>>>> >>>>> As far as I know, no. Both of these numbers are calculated by the >>>>> metamath-exe tool, using the command "SHOW TRACE_BACK 2p2e4 >>>>> /COUNT_STEPS". >>>>> Internally, it only creates and manipulates the numbers, it doesn't >>>>> actually perform the expansion (which would take exponentially long just >>>>> to >>>>> output). For the former number (12178 steps), an approximation to this is >>>>> to just "show proof *" which will print all proofs, or look at the entire >>>>> metamath web site on disk, which contains every step of every theorem. >>>>> The >>>>> 12178 steps are a subset of those, and you can get metamath-exe to print >>>>> out all of the relevant theorems using "show trace_back 2p2e4" alone. >>>>> >>>>> That said, it is certainly possible to calculate the actual 5.9 x >>>>> 10^12 steps if you are interested in such a programming project. But be >>>>> aware that the steps can also get pretty large in the process (I think >>>>> also >>>>> exponential in general). Although I'm sure your terabyte drive has better >>>>> things to do... >>>>> >>>>> Mario Carneiro >>>>> >>>>> On Mon, Apr 1, 2024 at 9:44 AM Anarcocap-socdem < >>>>> [email protected]> wrote: >>>>> >>>>>> Hello, I am trying to understand 2p2e4, as an excuse to understand >>>>>> metamath better. >>>>>> >>>>>> I have a few questions: >>>>>> >>>>>> 1. In https://us.metamath.org/mpeuni/mmset.html#trivia, it is stated >>>>>> that "A longest path back to an axiom from 2 + 2 = 4 is *184 layers* >>>>>> deep". However, if I run show trace_back 2p2e4 /count_steps, it is >>>>>> stated that "The maximum path length is 84". Is there a typo somewhere? >>>>>> (84 >>>>>> != 184). >>>>>> 2. If I run show trace_back 2p2e4 /count_steps, it is stated that " a >>>>>> total of 619 different subtheorems are used. The statement and >>>>>> subtheorems >>>>>> have a total of 12178 actual steps (...) The proof would have >>>>>> 5887862241803 >>>>>> =~ 5.9 x 10^12 steps if fully expanded back to axiom references.". What >>>>>> is >>>>>> the difference between the 12178 steps, and the 5.9 x 10^12 steps? I >>>>>> guess >>>>>> that 12178 steps refers to the case in which we take the axioms of the >>>>>> complex numbers as "axioms", and 5.9 x 10^12 when we also prove the >>>>>> axioms >>>>>> of the complex numbers, starting from ZFC. But I am not 100% sure, and I >>>>>> would like to have confirmation of that. >>>>>> 3. Is there some way to print/export to file the 12178 steps, and >>>>>> even the 5.9 x 10^12 steps, all at once? I ask this since running show >>>>>> trace_back 2p2e4 /tree gives me a tree, but with only the name of the >>>>>> subtheorems, not the steps themselves. And I have been unable to find a >>>>>> command that gives the full number of steps, all at the same time. >>>>>> >>>>>> Thank you for your work on this great project. >>>>>> >>>>>> -- >>>>>> 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/f3cb2f43-8608-4293-b2da-af283d9676fen%40googlegroups.com >>>>>> >>>>>> <https://groups.google.com/d/msgid/metamath/f3cb2f43-8608-4293-b2da-af283d9676fen%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/68e0c4f9-d0c4-4261-a949-610bdbd772ebn%40googlegroups.com >>>> >>>> <https://groups.google.com/d/msgid/metamath/68e0c4f9-d0c4-4261-a949-610bdbd772ebn%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/6300ff6f-9d28-468a-9716-589787a2e2e4n%40googlegroups.com >> >> <https://groups.google.com/d/msgid/metamath/6300ff6f-9d28-468a-9716-589787a2e2e4n%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/634f705b-58d1-477f-9c4a-c8a29d9a9b70n%40googlegroups.com.
