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"? 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.
