<abstract xmlns="http://www.w3.org/1999/xhtml"><p>In this article we prove the Leibniz series for <italic>π</italic> which states that
<disp-formula><alternatives><graphic xmlns:xlink="http://www.w3.org/1999/xlink" xlink:href="graphic/j_forma-2016-0023_eq_001.png"></graphic><math xmlns:mml="http://www.w3.org/1998/Math/MathML" display="block"><mfrac><mi>π</mi><mn>4</mn></mfrac><mo>=</mo><mstyle displaystyle="true"><munderover><mo>∑</mo><mrow><mi>n</mi><mo>=</mo><mn>0</mn></mrow><mi>∞</mi></munderover><mrow><mfrac><mrow><msup><mrow><mrow><mo>(</mo><mrow><mo>−</mo><mn>1</mn></mrow><mo>)</mo></mrow></mrow><mi>n</mi></msup></mrow><mrow><mn>2</mn><mo>⋅</mo><mi>n</mi><mo>+</mo><mn>1</mn></mrow></mfrac><mo>.</mo></mrow></mstyle></math><tex-math>$${\pi \over 4} = \sum\limits_{n = 0}^\infty {{{\left( { - 1} \right)^n } \over {2 \cdot n + 1}}.} $$</tex-math></alternatives></disp-formula></p><p>The formalization follows K. Knopp [<xref ref-type="bibr" rid="j_forma-2016-0023_ref_008_w2aab2b8b2b1b7b1ab1ab8Aa">8</xref>], [<xref ref-type="bibr" rid="j_forma-2016-0023_ref_001_w2aab2b8b2b1b7b1ab1ab1Aa">1</xref>] and [<xref ref-type="bibr" rid="j_forma-2016-0023_ref_006_w2aab2b8b2b1b7b1ab1ab6Aa">6</xref>]. <italic>Leibniz’s Series for Pi</italic> is item #26 from the “Formalizing 100 Theorems” list maintained by Freek Wiedijk at <ext-link ext-link-type="uri" xmlns:xlink="http://www.w3.org/1999/xlink" xlink:href="http://www.cs.ru.nl/F.Wiedijk/100/">http://www.cs.ru.nl/F.Wiedijk/100/</ext-link>.</p></abstract>

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/.

Leibniz Series for <italic>π</italic>

Institute of Informatics, University of Białystok, Ciołkowskiego 1M, 15-245 Białystok,

Formalized Mathematics

This work is licensed under version 3.0 of the Creative Commons Attribution–ShareAlike License.

{"article-title":{"italic":"π","content":"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...

Leibniz Series for π

Published Online: Feb 23, 2017

Page range: 275 - 280

Received: Oct 18, 2016

DOI: https://doi.org/10.1515/forma-2016-0023

Keywords
approximation, Leibniz theorem, Leibniz series

© 2016 Karol Pąk, published by De Gruyter Open

This work is licensed under version 3.0 of the Creative Commons Attribution–ShareAlike License.

Leibniz Series for π

Published Online: Feb 23, 2017

Page range: 275 - 280

Received: Oct 18, 2016

DOI: https://doi.org/10.1515/forma-2016-0023

Keywordsapproximation, Leibniz theorem, Leibniz series

© 2016 Karol Pąk, published by De Gruyter Open

This work is licensed under version 3.0 of the Creative Commons Attribution–ShareAlike License.

Keywords
approximation, Leibniz theorem, Leibniz series