{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,10]],"date-time":"2026-01-10T02:22:22Z","timestamp":1768011742151,"version":"3.49.0"},"reference-count":20,"publisher":"Walter de Gruyter GmbH","issue":"4","license":[{"start":{"date-parts":[[2016,12,1]],"date-time":"2016-12-01T00:00:00Z","timestamp":1480550400000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/creativecommons.org\/licenses\/by-sa\/3.0"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2016,12,1]]},"abstract":"<jats:title>Summary<\/jats:title>\n               <jats:p>In this article we prove the Leibniz series for <jats:italic>\u03c0<\/jats:italic> which states that\n<jats:disp-formula>\n                     <jats:alternatives>\n                        <jats:graphic xmlns:xlink=\"http:\/\/www.w3.org\/1999\/xlink\" xlink:href=\"graphic\/j_forma-2016-0023_eq_001.png\"\/>\n                        <m:math xmlns:m=\"http:\/\/www.w3.org\/1998\/Math\/MathML\" display=\"block\">\n                           <m:mfrac>\n                              <m:mi>\u03c0<\/m:mi>\n                              <m:mn>4<\/m:mn>\n                           <\/m:mfrac>\n                           <m:mo>=<\/m:mo>\n                           <m:mstyle displaystyle=\"true\">\n                              <m:munderover>\n                                 <m:mo>\u2211<\/m:mo>\n                                 <m:mrow>\n                                    <m:mi>n<\/m:mi>\n                                    <m:mo>=<\/m:mo>\n                                    <m:mn>0<\/m:mn>\n                                 <\/m:mrow>\n                                 <m:mi>\u221e<\/m:mi>\n                              <\/m:munderover>\n                              <m:mrow>\n                                 <m:mfrac>\n                                    <m:mrow>\n                                       <m:msup>\n                                          <m:mrow>\n                                             <m:mrow>\n                                                <m:mo>(<\/m:mo>\n                                                <m:mrow>\n                                                   <m:mo>\u2212<\/m:mo>\n                                                   <m:mn>1<\/m:mn>\n                                                <\/m:mrow>\n                                                <m:mo>)<\/m:mo>\n                                             <\/m:mrow>\n                                          <\/m:mrow>\n                                          <m:mi>n<\/m:mi>\n                                       <\/m:msup>\n                                    <\/m:mrow>\n                                    <m:mrow>\n                                       <m:mn>2<\/m:mn>\n                                       <m:mo>\u22c5<\/m:mo>\n                                       <m:mi>n<\/m:mi>\n                                       <m:mo>+<\/m:mo>\n                                       <m:mn>1<\/m:mn>\n                                    <\/m:mrow>\n                                 <\/m:mfrac>\n                                 <m:mo>.<\/m:mo>\n                              <\/m:mrow>\n                           <\/m:mstyle>\n                        <\/m:math>\n                        <jats:tex-math>$${\\pi \\over 4} = \\sum\\limits_{n = 0}^\\infty {{{\\left( { - 1} \\right)^n } \\over {2 \\cdot n + 1}}.} $$<\/jats:tex-math>\n                     <\/jats:alternatives>\n                  <\/jats:disp-formula>\n               <\/jats:p>\n               <jats:p>The formalization follows K. Knopp [8], [1] and [6]. <jats:italic>Leibniz\u2019s Series for Pi<\/jats:italic> is item #26 from the \u201cFormalizing 100 Theorems\u201d list maintained by Freek Wiedijk at <jats:ext-link xmlns:xlink=\"http:\/\/www.w3.org\/1999\/xlink\" ext-link-type=\"uri\" xlink:href=\"http:\/\/www.cs.ru.nl\/F.Wiedijk\/100\/\">http:\/\/www.cs.ru.nl\/F.Wiedijk\/100\/<\/jats:ext-link>.<\/jats:p>","DOI":"10.1515\/forma-2016-0023","type":"journal-article","created":{"date-parts":[[2017,2,25]],"date-time":"2017-02-25T10:00:53Z","timestamp":1488016853000},"page":"275-280","source":"Crossref","is-referenced-by-count":1,"title":["Leibniz Series for <i>\u03c0<\/i>"],"prefix":"10.1515","volume":"24","author":[{"given":"Karol","family":"P\u0105k","sequence":"first","affiliation":[{"name":"Institute of Informatics, University of Bia\u0142ystok, Cio\u0142kowskiego 1M, 15-245 Bia\u0142ystok, Poland"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"374","published-online":{"date-parts":[[2017,2,23]]},"reference":[{"key":"2021040806354289798_j_forma-2016-0023_ref_001_w2aab2b8b2b1b7b1ab1ab1Aa","doi-asserted-by":"crossref","unstructured":"[1] George E. Andrews, Richard Askey, and Ranjan Roy. Special Functions. Cambridge University Press, 1999.","DOI":"10.1017\/CBO9781107325937"},{"key":"2021040806354289798_j_forma-2016-0023_ref_002_w2aab2b8b2b1b7b1ab1ab2Aa","unstructured":"[2] Grzegorz Bancerek. The fundamental properties of natural numbers. Formalized Mathematics, 1(1):41\u201346, 1990."},{"key":"2021040806354289798_j_forma-2016-0023_ref_003_w2aab2b8b2b1b7b1ab1ab3Aa","unstructured":"[3] Czes\u0142aw Byli\u0144ski. The complex numbers. Formalized Mathematics, 1(3):507\u2013513, 1990."},{"key":"2021040806354289798_j_forma-2016-0023_ref_004_w2aab2b8b2b1b7b1ab1ab4Aa","unstructured":"[4] Czes\u0142aw Byli\u0144ski. Functions and their basic properties. Formalized Mathematics, 1(1): 55\u201365, 1990."},{"key":"2021040806354289798_j_forma-2016-0023_ref_005_w2aab2b8b2b1b7b1ab1ab5Aa","unstructured":"[5] Czes\u0142aw Byli\u0144ski. Functions from a set to a set. Formalized Mathematics, 1(1):153\u2013164, 1990."},{"key":"2021040806354289798_j_forma-2016-0023_ref_006_w2aab2b8b2b1b7b1ab1ab6Aa","doi-asserted-by":"crossref","unstructured":"[6] Lokenath Debnath. The Legacy of Leonhard Euler: A Tricentennial Tribute. World Scientific, 2010.","DOI":"10.1142\/p698"},{"key":"2021040806354289798_j_forma-2016-0023_ref_007_w2aab2b8b2b1b7b1ab1ab7Aa","unstructured":"[7] Noboru Endou, Katsumi Wasaki, and Yasunari Shidama. Definition of integrability for partial functions from \u211d to \u211d and integrability for continuous functions. Formalized Mathematics, 9(2):281\u2013284, 2001."},{"key":"2021040806354289798_j_forma-2016-0023_ref_008_w2aab2b8b2b1b7b1ab1ab8Aa","unstructured":"[8] Konrad Knopp. Infinite Sequences and Series. Dover Publications, 1956. ISBN 978-0-486-60153-3."},{"key":"2021040806354289798_j_forma-2016-0023_ref_009_w2aab2b8b2b1b7b1ab1ab9Aa","unstructured":"[9] Jaros\u0142aw Kotowicz. Partial functions from a domain to the set of real numbers. Formalized Mathematics, 1(4):703\u2013709, 1990."},{"key":"2021040806354289798_j_forma-2016-0023_ref_010_w2aab2b8b2b1b7b1ab1ac10Aa","unstructured":"[10] Jaros\u0142aw Kotowicz. Monotone real sequences. Subsequences. Formalized Mathematics, 1 (3):471\u2013475, 1990."},{"key":"2021040806354289798_j_forma-2016-0023_ref_011_w2aab2b8b2b1b7b1ab1ac11Aa","unstructured":"[11] Jaros\u0142aw Kotowicz. Real sequences and basic operations on them. Formalized Mathematics, 1(2):269\u2013272, 1990."},{"key":"2021040806354289798_j_forma-2016-0023_ref_012_w2aab2b8b2b1b7b1ab1ac12Aa","unstructured":"[12] Jaros\u0142aw Kotowicz. Convergent real sequences. Upper and lower bound of sets of real numbers. Formalized Mathematics, 1(3):477\u2013481, 1990."},{"key":"2021040806354289798_j_forma-2016-0023_ref_013_w2aab2b8b2b1b7b1ab1ac13Aa","unstructured":"[13] Rafa\u0142 Kwiatek. Factorial and Newton coefficients. Formalized Mathematics, 1(5):887\u2013890, 1990."},{"key":"2021040806354289798_j_forma-2016-0023_ref_014_w2aab2b8b2b1b7b1ab1ac14Aa","doi-asserted-by":"crossref","unstructured":"[14] Xiquan Liang and Bing Xie. Inverse trigonometric functions arctan and arccot. Formalized Mathematics, 16(2):147\u2013158, 2008. doi:10.2478\/v10037-008-0021-3.","DOI":"10.2478\/v10037-008-0021-3"},{"key":"2021040806354289798_j_forma-2016-0023_ref_015_w2aab2b8b2b1b7b1ab1ac15Aa","unstructured":"[15] Akira Nishino and Yasunari Shidama. The Maclaurin expansions. Formalized Mathematics, 13(3):421\u2013425, 2005."},{"key":"2021040806354289798_j_forma-2016-0023_ref_016_w2aab2b8b2b1b7b1ab1ac16Aa","unstructured":"[16] Chanapat Pacharapokin, Kanchun, and Hiroshi Yamazaki. Formulas and identities of trigonometric functions. Formalized Mathematics, 12(2):139\u2013141, 2004."},{"key":"2021040806354289798_j_forma-2016-0023_ref_017_w2aab2b8b2b1b7b1ab1ac17Aa","unstructured":"[17] Konrad Raczkowski. Integer and rational exponents. Formalized Mathematics, 2(1):125\u2013130, 1991."},{"key":"2021040806354289798_j_forma-2016-0023_ref_018_w2aab2b8b2b1b7b1ab1ac18Aa","unstructured":"[18] Konrad Raczkowski and Andrzej N\u0119dzusiak. Real exponents and logarithms. Formalized Mathematics, 2(2):213\u2013216, 1991."},{"key":"2021040806354289798_j_forma-2016-0023_ref_019_w2aab2b8b2b1b7b1ab1ac19Aa","unstructured":"[19] Piotr Rudnicki and Andrzej Trybulec. Abian\u2019s fixed point theorem. Formalized Mathematics, 6(3):335\u2013338, 1997."},{"key":"2021040806354289798_j_forma-2016-0023_ref_020_w2aab2b8b2b1b7b1ab1ac20Aa","unstructured":"[20] Yuguang Yang and Yasunari Shidama. Trigonometric functions and existence of circle ratio. Formalized Mathematics, 7(2):255\u2013263, 1998."}],"container-title":["Formalized Mathematics"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/content.sciendo.com\/view\/journals\/forma\/24\/4\/article-p275.xml","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/www.sciendo.com\/article\/10.1515\/forma-2016-0023","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,9]],"date-time":"2021-04-09T01:24:26Z","timestamp":1617931466000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.sciendo.com\/article\/10.1515\/forma-2016-0023"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016,12,1]]},"references-count":20,"journal-issue":{"issue":"4","published-online":{"date-parts":[[2017,2,23]]},"published-print":{"date-parts":[[2016,12,1]]}},"alternative-id":["10.1515\/forma-2016-0023"],"URL":"https:\/\/doi.org\/10.1515\/forma-2016-0023","relation":{},"ISSN":["1898-9934","1426-2630"],"issn-type":[{"value":"1898-9934","type":"electronic"},{"value":"1426-2630","type":"print"}],"subject":[],"published":{"date-parts":[[2016,12,1]]}}}