3 ms·
No. It's pretty common to have depth 20+ on even relatively simple proofs when you start looking at decomposing proofs to their axioms. The old joke about 1 +
by llm_trw 2y ago
No. It's pretty common to have depth 20+ on even relatively simple proofs when you start looking at decomposing proofs to their axioms.
The old joke about 1 + 1 = 2 being on page 360 of Principia Mathematica still largely holds.
- auggierose 2y agoThat depends on the granularity of your proof steps. That old joke doesn't hold for a very long time now (take a look at Isabelle/Isar proofs), yet people keep bringing it up.
- llm_trw 2y agoDoesn't matter what the granularity of your proof step is you still need to understand what that proof step does to be a mathematician. You seem to mistake syntactic brevity for semantic meaning.
- auggierose 2y agoMathematicians do very large proof steps, and so can the computer these days. If you do something like (proof by auto: thm_1 thm_2 thm_3) and it goes through, then I know why the proof works (because of these theorems), and this is similar to how a mathematician understands something. Syntactic brevity is indeed an indicator that you understand the proof. The better you understand something, the more concise you can formulate and prove it.