How rigorous are pictorial proofs?

The standard proof that $|\mathbb{Q}| = \mathbb{|N|}$ is pictorial. I am sure everyone here has seen it. The "zig-zag". I must admit, however, that, although I was "intuitively" convinced by it, I was never entirely satisfied with it because it is not an explicit bijection $f:\mathbb{N} \to \mathbb{Q}$ given by an actual formula. The fact that the proof is correct seems "clear" to us, but this is, again, merely an appeal to intuition. One should note that some of these "proofs by picture" are simply incorrect: see Russell O'Connor's answer here .

I have two questions

Is the pictorial proof that $|\mathbb{Q}| = \mathbb{|N|}$ rigorous by the standards of modern pure mathematics?

For the sake of this question, suppose that there isn't an explicit formla, or that it's too unwieldy to use in practice. After all, even if there is a formula, most of the people who've seen the pictorial argument do not know of it.

Is there an explicit formula for the "pictorial" proof?

There's some minor issues, of course, namely the inclusion of $0$ and variations of the "zig-zag" path, but these are no big deal. A bijection $f:\mathbb{N} \to \mathbb{N} \times \mathbb{N}$ suffices; dealing with negatives, equivalent fractions, etc is trivial.

I had the same question with the same proof (the zig-zag proof you are mentioning). At some point I decided to produce a formal proof.

Define a bijective function $f\colon \mathbb N \times \mathbb N \to \mathbb N$.

First of all you notice that going zig and then zag only helps intuition. In fact you don't need a "continuous" curve, so it is easier to go zig and the zig again... (so to speak). Then it is easy to count how many points you need to fill the first $k$ diagonals (sum of a arithmetic series: $k(k+1)/2$). The couple $(n,m)$ lies on the diagonal number $k=n+m$ so you easily find: $$ f(n,m) = \frac{(n+m)(n+m+1)}{2} + m = \frac{n^2+m^2+2nm+3m+n}{2}. $$

This was a little bit shocking to me! The function I was looking for is as simple as a polynomial... I would have expected some modulus, or some strange discontinuous function.

Nevertheless the algebraic proof that $f$ is bijective is not so simple... but following the intuition of the construction it is easy to write it.

What can we learn from this? The pictorial proof is for sure the best to understand a result and to remember it. Then it might happen that the abstract mathematics is even simpler than our intuition. Not always simple mathematics corresponds to simple pictures.

I suppose if you really wanted to, you could come up with an explicit bijection associated with the "zig-zag" proof. If that turns out to be difficult, you could come up with a different "zig-zag" that may have a simpler bijection. Although, the "zig-zag" proof is really just providing some intuitive backing to this theorem:

The union of a countable number of finite sets is countable.

Thinking of each diagonal of the "zig-zag" as one of your finite sets, and noting that every rational number has to be in one of those diagonals is sufficient to prove that $|\mathbb{Q}| = |\mathbb{N}|$.

On a more general note, the whole point of a proof is to clearly and correctly convey why a theorem is true. Sometimes it is easiest to convey why through written words, especially when the proof is long, relies on lemmas or the theorems of others, or just has lots of cases. But if there is a clever reason why a theorem is true, some clever "ah-HA" that you just have to see, a "proof by picture" can be much more clear than a formal write-up of a proof. The hope is, though, that after a reader sees a pictorial proof, they should have enough intuition into why the theorem is true to write up a formal proof if they really needed.

After seeing the "zig-zag" proof, do you think you can prove that the union of a countable number of finite sets is countable?

Munkres' "Topology" gives both the zig-zag intuition, and the actual formula for the bijection, as a good reference.

I read in an article (cannot remember the author, sadly) that proofs are not supposed to be 'entirely' rigorous. 'Proofs' try to convince the reader that it is possible to construct a completely rigorous proof. As in this case, although I too was not satisfied with the zig-zag-proof, it conveys the idea that the bijection does exists (without explicitly writing it out), and thus it is countable.