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.
