Hacker News Reader

Comment by disconcision | Hacker News Reader

not obviously the case. natural language also has tree/dag structure yet transformers do okay with it. encoding higher order structure in linear sequences seems necessary for transformers to be able to do most anything

View on HN

Not to arbitrary depth. Empirically the majority of text has depth less than 6 when represented as a tree. Proofs on the other hand have no a priori limits to their depth.

But isn't math strucutured in the same way subdivided in lemmas, theorems, corollarys with limited depth.

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.

That 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.

Doesn'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.

Mathematicians 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.

Reply on news.ycombinator.com