A ray in a graph $G=(V,E)$ is a sequence $X$ (possibly infinite) of distinct vertices $x_{0},x_{1},\ldots$ such that, for every $i$, $E(x_{i},x_{i+1})$. A classical theorem of graph theory (Halin [1965]) states that if a graph has, for each $k\in\mathbb{N}$, a set of $k$ many disjoint (say no vertices in common) infinite rays then there is an infinite sequence of disjoint infinite rays. The proof seems like an elementary argument by induction that uses the finite version of Menger's theorem at each step. One would thus expect the theorem to follow by very elementary (even computable) methods plus a compactness argument. We show that this is not the case. Indeed, the construction of the infinite set of disjoint rays is much more complicated. It occupies a level of complexity previously inhabited by a number of logical principals and only one fact from the mathematical literature. Such theorems are called theorems of hyperarithmetic analysis. Formally this means that they imply (in $\omega$-models) that for every set $A$ all transfinite iterations (through well-orderings computable from $A$) of the Turing jump beginning with $A$ exist. On the other hand, they are true in the ($\omega$-model) consisting of the subsets of $\mathbb{N}$ generated from any single set $A$ by these jump iterations. There are many variations of this theorem in the graph theory literature, for example, restricting to directed graphs, asking for edge disjointness or copies of double rays (order type $\mathbb{Z}$). These supply several other examples of theorems of hyperarithmetic analysis. This is joint work with James Barnes and Jun Le Goh