> 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 < jordi.molins.coron...@gmail.com> 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 metamath+unsubscr...@googlegroups.com. > 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 metamath+unsubscr...@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/CAFXXJSvJ80e936ACQPCvYWFg%3DFtEx05-P8ssFGU64sV24KCPdQ%40mail.gmail.com.
