elementary set theory - 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.

Answer

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.