Abstract: 
This work contains a proof of Stirling's formula both for the factorial $n! \sim \sqrt{2\pi n} (n/e)^n$ on natural numbers and the real
Gamma function $\Gamma(x)\sim \sqrt{2\pi/x} (x/e)^x$. The proof is based on work by Graham Jameson.
This is then extended to the full asymptotic expansion
$$\log\Gamma(z) = \big(z  \tfrac{1}{2}\big)\log z  z + \tfrac{1}{2}\log(2\pi) + \sum_{k=1}^{n1} \frac{B_{k+1}}{k(k+1)} z^{k}\\
{}  \frac{1}{n} \int_0^\infty B_n([t])(t + z)^{n}\,\text{d}t$$
uniformly for all complex $z\neq 0$ in the cone $\text{arg}(z)\leq \alpha$ for any $\alpha\in(0,\pi)$, with which the above asymptotic
relation for Γ is also extended to complex arguments. 
BibTeX: 
@article{Stirling_FormulaAFP,
author = {Manuel Eberl},
title = {Stirling's formula},
journal = {Archive of Formal Proofs},
month = sep,
year = 2016,
note = {\url{https://isaafp.org/entries/Stirling_Formula.html},
Formal proof development},
ISSN = {2150914x},
}
