The Coq mailing list

[Gabriel Scherer <gabriel.scherer AT gmail.com>]

There may be a misunderstanding about this equality. It is "obviously
false" in the sense that the standard, commonly accepted of what it
"means" to write an infinite summation is that it means the limit of
the sequence of partial summations, if it exists, and does not mean
anything. This equality does not mean anything by this criteria, so
you could say it is "false".

Now, you may always play on words, suspend disbelief, and extend your
number space with abstract infinite series, whose algebraic properties
you would study. Properties which may allow you to prove that, in this
extended funny space, the abstract series S at hands verifies 12*S + 1
= 0. Or maybe you can play on words differently, and justify the limit
by continuous extension of the Zeta function -- but be careful,
because justifications from algebra and analysis sometimes differ in
their results. In this case it happens that various ways to play on
words tend to be consistent in suggesting -1/12 as a plausible
extension of meaning, and that physicists work on objects that are
compatible with some of those extensions, and have been therefore
relying on similar techniques to avoid divergence of their models.

But a shiny Youtube video does not change the fact that the summation
is trivially divergent. Do we really need to prove that in Coq? What
do you want?

On Mon, Feb 3, 2014 at 10:11 PM, Kevin Sullivan
<sullivan.kevinj AT gmail.com>
 wrote:
> Has anyone on this list taken a shot at formalizing the proposition that the
> sum of all the natural numbers is 1/12, or the negation? This video was
> referenced by a recent NYT article.
>
> http://www.youtube.com/watch?v=w-I6XTVZXww#t=420
>
> Regards,
> Kevin Sullivan