One of my first blog posts is about a cool double summation identity:
\[\sum_{n=2}^{\infty} \sum_{p=2}^{\infty} \frac{1}{n^p} = 1\]
The proof is short and sweet, so I thought it’d be a nice exercise to formalize it in Lean. So, here’s my proof.
Was it nice? Nope, it was over 250 lines of mostly fraction manipulation and annoying casts between natural numbers and reals. I recommend opening up the proof in a Lean editor to see the hypotheses and goal state at each line, since otherwise you’ll be in the dark about what’s going on.
I don’t know much real analysis, so I’m not entirely sure if my proof’s definition of double summation convergence is correct, since my definition always allows switching the order of the summations which seems sketchy. Also, I’d gladly appreciate tips on how to simplify or shorten the proof since it’s much, much longer than the equivalent pencil-and-paper proof of the same identity.
Some helpful resources I used to write the proof: