Leibniz Series for π

In this article we prove the Leibniz series for π which states that π4=∑n=0∞(−1)n2⋅n+1.$${\pi \over 4} = \sum\limits_{n = 0}^\infty {{{\left( { - 1} \right)^n } \over {2 \cdot n + 1}}.} $$

The formalization follows K. Knopp [8], [1] and [6]. Leibniz’s Series for Pi is item #26 from the “Formalizing 100 Theorems” list maintained by Freek Wiedijk at http://www.cs.ru.nl/F.Wiedijk/100/.