I'm sure that we've all seen diagrams such as this to show how we can order sets such as the rationals in order to show that they are countable, however, is there a way to find the nth term of such a list? Can it be expressed as a formula? Or does this require some sort of algorithm?
Furthermore, can this be done without any informal appeal to "the nth line"?
Let $$f:\mathbb R \to \mathbb R, f(x) := \frac{x(x+1)}2 $$ $f(n)-f(n-1)=n$ for every $n \in \mathbb N$.
Also, $f(x)$ is one-to-one when $x \geq 0$.
The bijection you want is $$u_n=(n-f\left(\lfloor f^{-1}(n)\rfloor\right),f\left(\lfloor f^{-1}(n)\rfloor+1\right)-n-1) $$
Proof of surjectivity: Given $(a,b) \in \mathbb N \times \mathbb N$, make $n=f(a+b)+a$. Then $u_n=(a,b)$.