{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,30]],"date-time":"2026-03-30T11:04:53Z","timestamp":1774868693513,"version":"3.50.1"},"reference-count":14,"publisher":"Walter de Gruyter GmbH","issue":"1","license":[{"start":{"date-parts":[[2025,9,1]],"date-time":"2025-09-01T00:00:00Z","timestamp":1756684800000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by-sa\/4.0"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2025,9,1]]},"abstract":"<jats:title>Summary<\/jats:title>\n                  <jats:p>\n                    In this article, we formalized the proof of the Stirling\u2019s formula, which is considered an essential item in the field of statistics, as shown below:\n                    <jats:disp-formula>\n                      <jats:alternatives>\n                        <jats:graphic xmlns:xlink=\"http:\/\/www.w3.org\/1999\/xlink\" xlink:href=\"graphic\/j_forma-2025-0008_eq_001.png\"\/>\n                        <m:math xmlns:m=\"http:\/\/www.w3.org\/1998\/Math\/MathML\" display=\"block\">\n                          <m:mrow>\n                            <m:munder>\n                              <m:mrow>\n                                <m:mo>lim<\/m:mo>\n                              <\/m:mrow>\n                              <m:mrow>\n                                <m:mi>n<\/m:mi>\n                                <m:mo>\u2192<\/m:mo>\n                                <m:mo>\u221e<\/m:mo>\n                              <\/m:mrow>\n                            <\/m:munder>\n                            <m:mfrac>\n                              <m:mrow>\n                                <m:mi>n<\/m:mi>\n                                <m:mo>!<\/m:mo>\n                              <\/m:mrow>\n                              <m:mrow>\n                                <m:msup>\n                                  <m:mrow>\n                                    <m:mi>n<\/m:mi>\n                                  <\/m:mrow>\n                                  <m:mrow>\n                                    <m:mi>n<\/m:mi>\n                                    <m:mo>+<\/m:mo>\n                                    <m:mfrac>\n                                      <m:mn>1<\/m:mn>\n                                      <m:mn>2<\/m:mn>\n                                    <\/m:mfrac>\n                                  <\/m:mrow>\n                                <\/m:msup>\n                                <m:msup>\n                                  <m:mrow>\n                                    <m:mi>e<\/m:mi>\n                                  <\/m:mrow>\n                                  <m:mrow>\n                                    <m:mo>-<\/m:mo>\n                                    <m:mi>n<\/m:mi>\n                                  <\/m:mrow>\n                                <\/m:msup>\n                              <\/m:mrow>\n                            <\/m:mfrac>\n                            <m:mo>=<\/m:mo>\n                            <m:msqrt>\n                              <m:mrow>\n                                <m:mn>2<\/m:mn>\n                                <m:mi>\u03c0<\/m:mi>\n                              <\/m:mrow>\n                            <\/m:msqrt>\n                          <\/m:mrow>\n                        <\/m:math>\n                        <jats:tex-math>\\mathop {\\lim }\\limits_{n \\to \\infty } {{n!} \\over {{n^{n + {1 \\over 2}}}{e^{ - n}}}} = \\sqrt {2\\pi }<\/jats:tex-math>\n                      <\/jats:alternatives>\n                    <\/jats:disp-formula>\n                    using the Mizar formalism.\n                  <\/jats:p>","DOI":"10.2478\/forma-2025-0008","type":"journal-article","created":{"date-parts":[[2025,12,24]],"date-time":"2025-12-24T23:55:15Z","timestamp":1766620515000},"page":"95-102","source":"Crossref","is-referenced-by-count":0,"title":["A Formal Proof of Stirling\u2019s Formula"],"prefix":"10.2478","volume":"33","author":[{"given":"Yasushige","family":"Watase","sequence":"first","affiliation":[{"name":"Faculty of Data Science University of Rissho Magechi Kumagaya , Japan"}]}],"member":"374","published-online":{"date-parts":[[2025,12,23]]},"reference":[{"key":"2026033010152112951_j_forma-2025-0008_ref_001","doi-asserted-by":"crossref","unstructured":"Yves Bertot. A short presentation of Coq. In Otmane A\u00eft Mohamed, C\u00e9sar A. Mu\u00f1oz, and Sofi\u00e8ne Tahar, editors, Theorem Proving in Higher Order Logics (TPHOLs 2008), volume 5170 of LNCS, pages 12\u201316. Springer, 2008. doi:10.1007\/978-3-540-71067-73.","DOI":"10.1007\/978-3-540-71067-7_3"},{"key":"2026033010152112951_j_forma-2025-0008_ref_002","unstructured":"Richard Courant and Fritz John. Introduction to Calculus and Analysis I. John Wiley and Sons Inc., New York, 1st edition, 1965."},{"key":"2026033010152112951_j_forma-2025-0008_ref_003","unstructured":"Manuel Eberl. Stirling\u2019s formula. Archive of Formal Proofs, September 2016. https:\/\/isa-afp.org\/entries\/Stirling_Formula.html, Formal proof development."},{"key":"2026033010152112951_j_forma-2025-0008_ref_004","doi-asserted-by":"crossref","unstructured":"Noboru Endou. Relationship between the Riemann and Lebesgue integrals. Formalized Mathematics, 29(4):185\u2013199, 2021. doi:10.2478\/forma-2021-0018.","DOI":"10.2478\/forma-2021-0018"},{"key":"2026033010152112951_j_forma-2025-0008_ref_005","doi-asserted-by":"crossref","unstructured":"Adam Grabowski, Artur Korni\u0142owicz, and Adam Naumowicz. Four decades of Mizar. Journal of Automated Reasoning, 55(3):191\u2013198, 2015. doi:10.1007\/s10817-015-9345-1.","DOI":"10.1007\/s10817-015-9345-1"},{"key":"2026033010152112951_j_forma-2025-0008_ref_006","unstructured":"John Harrison. Stirling\u2019s approximation. 2010. Available online at https:\/\/github.com\/jrh13\/hol-light\/blob\/master\/100\/stirling.ml."},{"key":"2026033010152112951_j_forma-2025-0008_ref_007","unstructured":"Nobushige Kurokawa. Modern Trigonometric Function Theory. Iwanami Shoten, Publishers (Tokyo), 1st edition, 2013. In Japanese."},{"key":"2026033010152112951_j_forma-2025-0008_ref_008","unstructured":"Norman D. Megill and David A. Wheeler. Metamath: A Computer Language for Mathematical Proofs. Lulu Press, Morrisville, North Carolina, 2019. http:\/\/us.metamath.org\/downloads\/metamath.pdf."},{"key":"2026033010152112951_j_forma-2025-0008_ref_009","doi-asserted-by":"crossref","unstructured":"Leonardo de Moura and Sebastian Ullrich. The Lean 4 theorem prover and programming language. In Automated Deduction \u2013 CADE 28: 28th International Conference on Automated Deduction, Virtual Event, July 12\u201315, 2021, Proceedings, pages 625\u2013635, Berlin, Heidelberg, 2021. Springer-Verlag. doi:10.1007\/978-3-030-79876-537.","DOI":"10.1007\/978-3-030-79876-5_37"},{"key":"2026033010152112951_j_forma-2025-0008_ref_010","unstructured":"Yasunari Shidama. The Taylor expansions. Formalized Mathematics, 12(2):195\u2013200, 2004."},{"key":"2026033010152112951_j_forma-2025-0008_ref_011","doi-asserted-by":"crossref","unstructured":"Yasushige Watase. Formal proof of transcendence of the number e. Part II. Formalized Mathematics, 32(1):121\u2013131, 2024. doi:10.2478\/forma-2024-0009.","DOI":"10.2478\/forma-2024-0009"},{"key":"2026033010152112951_j_forma-2025-0008_ref_012","doi-asserted-by":"crossref","unstructured":"Yasushige Watase. Formalization of Wallis infinite product formula for \u03c0 and the Wallis integral. Formalized Mathematics, 33(1):85\u201394, 2025. doi:10.2478\/forma-2025-0007.","DOI":"10.2478\/forma-2025-0007"},{"key":"2026033010152112951_j_forma-2025-0008_ref_013","unstructured":"Freek Wiedijk. Formalizing 100 theorems. Available online at http:\/\/www.cs.ru.nl\/~freek\/100\/."},{"key":"2026033010152112951_j_forma-2025-0008_ref_014","doi-asserted-by":"crossref","unstructured":"Rafa\u0142 Ziobro. Fermat\u2019s Little Theorem via divisibility of Newton\u2019s binomial. Formalized Mathematics, 23(3):215\u2013229, 2015. doi:10.1515\/forma-2015-0018.","DOI":"10.1515\/forma-2015-0018"}],"container-title":["Formalized Mathematics"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.sciendo.com\/pdf\/10.2478\/forma-2025-0008","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,3,30]],"date-time":"2026-03-30T10:15:51Z","timestamp":1774865751000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.sciendo.com\/article\/10.2478\/forma-2025-0008"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,9,1]]},"references-count":14,"journal-issue":{"issue":"1","published-online":{"date-parts":[[2025,12,23]]},"published-print":{"date-parts":[[2025,9,1]]}},"alternative-id":["10.2478\/forma-2025-0008"],"URL":"https:\/\/doi.org\/10.2478\/forma-2025-0008","relation":{},"ISSN":["1898-9934"],"issn-type":[{"value":"1898-9934","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,9,1]]}}}