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. 
 A: 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?
A: 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.
A: The point of something like the zig-zag proof is not to be rigorous in itself but instead to convince a mathematician that he or she could easily make the proof rigorous if pressed to do so by the gods of rigour.
Also, you can come up with very succinct surjections from N to Q. For example, map every natural number of the form $2^p 3^q 5^r $ to $(-1)^r p/q$. It's extremely easy now to see that if you give me a rational, there is a natural number which is mapped to it. 
The downside with this is that if you are teaching countability you would need to check that "surjection from" is the same as "bijection with", which sometimes hasn't been proved by this stage.
A: 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.
A: Pictures have their strengths and weaknesses, but they're just as rigorous as any other informal type of proof — that is, they may or may not be depending on how well written it is.
And the zig-zag proof is a rather clear depiction of an explicit algorithm for enumerating the rationals.
Regarding your particular doubts, I don't think it's really the picture that's the issue — it's that the function was defined by an algorithm for producing its values, rather than as an arithmetic formula.
Formal proofs can be 'pictures' too; you can develop formal logic in a way where the basic 'data type' is something other than strings of symbols. e.g. graphs of various sorts are often useful.
A: This doesn't directly address the proof of $|\mathbb{N}|=|\mathbb{Q}|$, but the more abstract notion of pictorial proofs as found in elementary geometry:
Avigad, Dean & Mumma A Formal System for Euclid's Elements:
http://repository.cmu.edu/philosophy/61/
They show that certain types of pictorial arguments that occur in Euclid's Elements, while apparently un-rigorous, can be described in a precise manner using formal rules, in a way that the conclusion follows directly from the pictorial "special case". In essence, a particular diagram can be in "general enough position" to allow rigorous conclusions to be drawn from it.
A: So... take the ordered pair $(n,m) $.  
The pictorial and non rigorous concept of the "diagonal"  is simply {$(j,k) | j+k=n+m; j\ge 0;k \ge 0$}. Note: there are $(n+m)+1$ terms in this diagonal
The previous diagonals had 1 term, two terms ... so on to $(n+m)$ terms.  So the previous diagonals account for $\sum_{i=1}^{n+m} i  = \frac {(n+m)(n+m+1)}{2} $ items.  
Starting at $(0,n+m) $ end of the diagonal $(n,m) $ is the $n +1$th item of the current diagonal.
So the bijection you want is $(n,m)\rightarrow \frac {(n+m)(n+m+1)}2 + n $.
$(0,0)\implies 0$
$(0,1)\implies 1$
$(1,0) \implies 2$
$(2,0) \implies 3$
$(1,1)\implies 4$
Etc. Algebraically it's probably easy to show this is injective .  Suppose (a,b) and (c,d) both map to t.
Case 1: a+b = c+d= K.  
Then $\frac {K (K+1)}{2} + a = \frac {K (K+1)}2 + b$.  So $a = c $.  So $b = c =K -a $.
Case 2:  Wolog a+b < c+d
$\frac {(a+b)(a+b+1)}2 + a \le \frac {(a+b)(a+b+1)}2 + (a+b)$
$=\frac {(a+b)(a+b+3)}2 $
$\le \frac {((c+d)-1)((c+d+1)+1)}2$
$=\frac {(c+d)(c+d +1) +(c+d) -(c+d+1)-1}2 $
$=\frac{(c+d)(c+d+1)}2 -1$
$< \frac{(c+d)(c+d+1)}2 + c $
Which is a contradiction.
So (a,b)=(c,d).
Proving it's surjective isn't nescessary though it is.
For each t there exist, k, so that $\frac {k (k+1)}2 \le t < \frac{(k+1)(k+2)}2$.
Let $n = t -\frac {k (k+1)}2 \ge 0$.  Let $m=k-n = k - t + \frac {k (k+1)}2 > k - \frac {(k+1)(k+2)}2 + \frac {k (k+1)}2=k +\frac {k+1}2 (k-(k+2))=k - (k+1)=-1$.  So $m \ge 0$
Then $(n,m)\rightarrow t$.
===
Anyway....
I don't think such an intensive arithmetic is nescessary.  What matters is the argument that it can be done.  As the diagonals increase by one each iteration, and as we can group the natural numbers into sequences of groups each increasing in terms by one, each group of natural numbers coresponds to a diagonal, and each of there natural numbers in the group corresponds to a term in the diagonal.  Thus must be shown but it needn't be shown by convoluted arithmetic.
