I wanted to go through the usual heuristic argument that
\[1+2+3+\cdots = -1/12\]
and see what about it I can believe in.
Manipulating Power Series
Here's a version of the story that starts with a power series in a variable $q$.
Define the function (thinking of $q$ as a real number, and $\alpha$ as a function $\R \to \R$)
\[\alpha(q) = {q\over (1-q)^2}\]
and observe it has a power series
\[\alpha(q) = q + 2q^2 + 3q^3 + 4q^4 + \cdots\]
Now try to compute $\alpha(q) + \alpha(-q)$. We find
\[\alpha(q) + \alpha(-q) = (q + 2q^2 + 3q^3 + 4q^4 + \cdots) + (-q + 2q^2 - 3q^3 + 4q^4 - \cdots)\]
\[ = 4q^2 + 8q^4 + 12q^3 + 16q^4 + \cdots\]
\[ = 4\alpha(q^2) \]
But now let's expand out $\alpha(-q)$ according to its definition:
\[\alpha(q) + {-q\over (1+q)^2} = 4\alpha(q^2)\]
Now multiply both sides by $(1+q)^2$:
\[\alpha(q)(1+q)^2 - {q} = 4\alpha(q^2)(1+q)^2\]
And move the $q$ to the right-hand side:
\[\alpha(q)(1+q)^2 = q + 4\alpha(q^2)(1+q)^2 \tag{\dag}\]
Interpreting as a Functional Program
Notice that we have completely gotten rid of any minus signs or divisions outside of $\alpha$.
This means we can Curry-Howard everything in sight: interpret multiplication as product types, addition as sum types,
1 as the unit type, 4 as a four-element type, and $\alpha$ as the type operator
\[\alpha(\tau) = (\tau, [\tau], [\tau])\]
using Haskell notation $[\tau]$ for the type of lists of $\tau$, and $(\tau_1, \tau_2, \ldots)$ for tuple types.
The equation $(\dag)$ becomes an (alleged!) isomorphism
of types:
\[(\alpha(\tau), (1+\tau), (1+\tau)) \cong \tau + (4, \alpha(\tau, \tau), (1+\tau), (1+\tau)) \]
Let's write $\tau?$ for the Maybe-type $(1 + \tau)$, and expand the definition of $\alpha$:
Now our claim is that
\[(\tau, [\tau], [\tau], \tau?, \tau?) \cong \tau + (4, \tau, \tau, [\tau, \tau], [\tau, \tau], \tau?, \tau?) \]
We can in fact realize this isomorphism as a simple functional program.
Let $\binl$ and $\binr$ be the injections into general sum types, and
$\bnone$ and $\bjust$ be injections into the type $\tau?$, and let
the elements of the four-element type be $4 = \{\ms 0, \ms 1, \ms 2, \ms 3\}$.
Define the following function:
\[\iso : (\tau, [\tau], [\tau], \tau?, \tau?) \to \tau + (4, \tau, \tau, [\tau], [\tau])\]
\[\begin{align*}
\iso(z, [], [], \bnone, \bnone) &= \binl z\\
\iso(z, xs, ys, \bjust u, \bnone) &= \binr (\ms0, z, u, xs, ys)\\
\iso(z, xs, ys, \bnone, \bjust u) &= \binr (\ms1, z, u, xs, ys)\\
\iso(z, xs, ys, \bjust x, \bjust u) &= \binr (\ms2, z, u, x \cc xs, ys)\\
\iso(z, [], y \cc ys, \bnone, \bnone) &= \binr (\ms2, z, y, [], ys)\\
\iso(z, x \cc xs, ys, \bnone, \bnone) &= \binr (\ms3, z, x, xs, ys)\\
\end{align*}\]
Notice that the definition $\iso$ covers all input cases uniquely. If
at least one of the two $\tau?$ arguments is $\bjust$, then the other variables
$z,xs,ys$ are consumed uniformly without further pattern matching. If both are
$\bnone$, then we can split cases first on whether the first $[\tau]$ argument is empty,
then on whether the second $[\tau]$ argument is empty.
Moreover, we can define the inverse of $\iso$ by simply reversing the left and right-hand sides
of each defining clause. Coverage checking of the right-hand sides of $\iso$ is also easy.
If we have an $\binl$, then no further pattern-matching of $z$ is required. If we have an $\binr$,
then we split cases on the (non)emptiness of the first $[\tau]$ only if the $4$ argument is $\ms 2$.
Note that $\iso$ isn't quite what we originally wanted to prove — its codomain is
\[\tau + (4, \tau, \tau, [\tau], [\tau])\] rather than
\[\tau + (4, \tau, \tau, [\tau, \tau], [\tau, \tau], \tau?, \tau?)\]
But we can observe that $[\tau]$ is easily seen to be isomorphic to $([\tau, \tau], \tau?)$, for any list
consists of an even-length list, together with maybe one remaining element if the original list happened to be of odd length.
This completes the proof that there is an isomorphism of types
\[(\tau, [\tau], [\tau], \tau?, \tau?) \cong \tau + (4, \tau, \tau, [\tau, \tau], [\tau, \tau], \tau?, \tau?) \]
Interpreting -1/12
The previous section is an actual definite truth about types and functions. If we switch our mindset
back to "heuristic suggestive informal real-number arguments" mode, and look again at
\[\alpha(q)(1+q)^2 = q + 4\alpha(q^2)(1+q)^2 \]
We notice that if we plug in $q=1$, we get
\[\alpha(1)\cdot 2^2 = 1 + 4\alpha(1)\cdot 2^2 \]
\[4\alpha(1) = 1 + 16\alpha(1) \]
\[(-12)\alpha(1) = 1 \]
\[\alpha(1) = -1/12 \]
So if we look at $\iso$ and substitute $\tau = 1$, we find we have exhibited an isomorphism
\[(1, [1], [1], 1?, 1?) \cong 1 + (4, 1, 1, [1, 1], [1, 1], 1?, 1?) \]
The analog of $\alpha(1)$ here is the type $(1,[1],[1]) = ([1],[1])$ of pairs of lists of unit.
But a list of unit is just a natural number, really, so in what sense is
\[(\N,\N) = 1 + 2 + 3 + \cdots\]
true? The interpretation goes that each summand $n$ on right-hand side collects together the pairs of numbers
that add up to $n-1$. Thus we're imagining that:
\[ 1 = \{(0,0)\}\qquad 2 = \{(0,1),(1,0)\} \qquad 3 = \{(0,2),(1,1),(2,0)\} \qquad \cdots\]
and then we claim
\[(1, [1], [1], 1?, 1?) \cong 1 + (4, 1, 1, [1, 1], [1, 1], 1?, 1?) \]
which is really the same thing as
\[((\N, \N), (1?, 1?)) \cong 1 + (4, (\N, \N), (1?, 1?))\]
which is also the same thing as
\[((\N, \N), (1?, 1?)) \cong ((\N, \N), (1?, 1?)) + 1 + ((3, 1?, 1?), (\N, \N))\]
So between the left-hand side and the right-hand side of this bijection, we have added
\[1 + ((3, 1?, 1?), (\N, \N))\]
So in some sense this type "behaves like zero" in this context, and it is one plus 12 (i.e. $(3, 1?, 1?)$)
times $(\N, \N)$. So that is the sense in which
\[1 + 2 + 3 + \cdots \cong (\N, \N) \approx -1/12\]