A Formal Proof of Stirling’s Formula

Summary 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: <m:math xmlns:m="http://www.w3.org/1998/Math/MathML" display="block"> <m:mrow> <m:munder> <m:mrow> <m:mo>lim</m:mo> </m:mrow> <m:mrow> <m:mi>n</m:mi> <m:mo>→</m:mo> <m:mo>∞</m:mo> </m:mrow> </m:munder> <m:mfrac> <m:mrow> <m:mi>n</m:mi> <m:mo>!</m:mo> </m:mrow> <m:mrow> <m:msup> <m:mrow> <m:mi>n</m:mi> </m:mrow> <m:mrow> <m:mi>n</m:mi> <m:mo>+</m:mo> <m:mfrac> <m:mn>1</m:mn> <m:mn>2</m:mn> </m:mfrac> </m:mrow> </m:msup> <m:msup> <m:mrow> <m:mi>e</m:mi> </m:mrow> <m:mrow> <m:mo>-</m:mo> <m:mi>n</m:mi> </m:mrow> </m:msup> </m:mrow> </m:mfrac> <m:mo>=</m:mo> <m:msqrt> <m:mrow> <m:mn>2</m:mn> <m:mi>π</m:mi> </m:mrow> </m:msqrt> </m:mrow> </m:math> \mathop {\lim }\limits_{n \to \infty } {{n!} \over {{n^{n + {1 \over 2}}}{e^{ - n}}}} = \sqrt {2\pi } using the Mizar formalism.