Re: [Metamath] Trying to understand 2p2e4

2024-04-01 Thread Mario Carneiro
> 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

[Metamath] Trying to understand 2p2e4

2024-04-01 Thread Anarcocap-socdem
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