A Formal Proof of Stirling’s Formula

Watase, Yasushige

doi:10.2478/forma-2025-0008

Abstract

In this article, we formalized the proof of the Stirling’s formula, which is considered an essential item in the field of statistics, as shown below: $lim_{n \to \infty} \frac{n!}{n^{n + \frac{1}{2}} e^{- n}} = \sqrt{2 π}$ \mathop {\lim }\limits_{n \to \infty } {{n!} \over {{n^{n + {1 \over 2}}}{e^{ - n}}}} = \sqrt {2\pi } using the Mizar formalism.

References

Yves Bertot. A short presentation of Coq. In Otmane Aït Mohamed, César A. Muñoz, and Sofiène Tahar, editors, Theorem Proving in Higher Order Logics (TPHOLs 2008), volume 5170 of LNCS, pages 12–16. Springer, 2008. doi:10.1007/978-3-540-71067-73.
Search in Google Scholar Back to article
Richard Courant and Fritz John. Introduction to Calculus and Analysis I. John Wiley and Sons Inc., New York, 1st edition, 1965.
Search in Google Scholar Back to article
Manuel Eberl. Stirling’s formula. Archive of Formal Proofs, September 2016. https://isa-afp.org/entries/Stirling_Formula.html, Formal proof development.
Search in Google Scholar Back to article
Noboru Endou. Relationship between the Riemann and Lebesgue integrals. Formalized Mathematics, 29(4):185–199, 2021. doi:10.2478/forma-2021-0018.
Search in Google Scholar Back to article
Adam Grabowski, Artur Korniłowicz, and Adam Naumowicz. Four decades of Mizar. Journal of Automated Reasoning, 55(3):191–198, 2015. doi:10.1007/s10817-015-9345-1.
Search in Google Scholar Back to article
John Harrison. Stirling’s approximation. 2010. Available online at https://github.com/jrh13/hol-light/blob/master/100/stirling.ml.
Search in Google Scholar Back to article
Nobushige Kurokawa. Modern Trigonometric Function Theory. Iwanami Shoten, Publishers (Tokyo), 1st edition, 2013. In Japanese.
Search in Google Scholar Back to article
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.
Search in Google Scholar Back to article
Leonardo de Moura and Sebastian Ullrich. The Lean 4 theorem prover and programming language. In Automated Deduction – CADE 28: 28th International Conference on Automated Deduction, Virtual Event, July 12–15, 2021, Proceedings, pages 625–635, Berlin, Heidelberg, 2021. Springer-Verlag. doi:10.1007/978-3-030-79876-537.
Search in Google Scholar Back to article
Yasunari Shidama. The Taylor expansions. Formalized Mathematics, 12(2):195–200, 2004.
Search in Google Scholar Back to article
Yasushige Watase. Formal proof of transcendence of the number e. Part II. Formalized Mathematics, 32(1):121–131, 2024. doi:10.2478/forma-2024-0009.
Search in Google Scholar Back to article
Yasushige Watase. Formalization of Wallis infinite product formula for π and the Wallis integral. Formalized Mathematics, 33(1):85–94, 2025. doi:10.2478/forma-2025-0007.
Search in Google Scholar Back to article
Freek Wiedijk. Formalizing 100 theorems. Available online at http://www.cs.ru.nl/~freek/100/.
Search in Google Scholar Back to article
Rafał Ziobro. Fermat’s Little Theorem via divisibility of Newton’s binomial. Formalized Mathematics, 23(3):215–229, 2015. doi:10.1515/forma-2015-0018.
Search in Google Scholar Back to article

A Formal Proof of Stirling’s Formula

Abstract

Paradigm

My account