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.
