The first "proof" I learned for why the rationals are countably infinite relied on arranging the rational numbers in a two-dimensional array and using the well-known traversal shown below to construct a bijection from $\mathbb{N}$ to $\mathbb{Q}$. (Note that the image is missing the nonpositive rational numbers; it is only meant to illustrate the algorithm used to form the list of rationals).
In short, whenever we encounter a new rational number along the path shown in the picture, we append it to a list. This list is the desired injection from $\mathbb{N}$ to $\mathbb{Q}$.
However, this proof is labeled as "informal" on ProofWiki. Instead, the "formal" proof constructs an injection $\phi : \mathbb{Q} \to \mathbb{Z} \times \mathbb{N}$, and uses the fact that Cartesian product of countable sets is countable. In what way is the "informal" proof lacking in rigor? Is it logically unsound?
Thanks for your insight!
The argument you mention is sound. The issue is with the proof not being very formal. The proof does not actually construct any bijection, instead it convinces you that you can construct a bijection by following a certain algorithm. If this proof contained a more explicit description of the algorithm together with a proof of its correctness (i.e., that it does produce a bijection (and notice here that this algorithm is only expected to yield the answer after infinitely many steps (this is not what we usually call a valid algorithm))) then it would be a formal proof.
So, while the informal idea is very convincing, turning it into a formal proof is rather tedious. Instead, the formal argument you mention hides the mess in the proof that a cartesian product of two countable sets is countable. This need to be proved as well (this is essentially the same as showing that $\mathbb Q$ is countable). One very clean way to formally prove this is to use the Cantor-Shroeder-Bernstein theorem.