Abstract: 
Bernoulli numbers were first discovered in the closedform
expansion of the sum 1^{m} +
2^{m} + … + n^{m}
for a fixed m and appear in many other places. This entry provides
three different definitions for them: a recursive one, an explicit
one, and one through their exponential generating function.
In addition, we prove some basic facts, e.g. their relation
to sums of powers of integers and that all odd Bernoulli numbers
except the first are zero. We also prove the correctness of the
Akiyama–Tanigawa algorithm for computing Bernoulli numbers
with reasonable efficiency, and we define the periodic Bernoulli
polynomials (which appear e.g. in the Euler–MacLaurin
summation formula and the expansion of the logGamma function) and
prove their basic properties. 
BibTeX: 
@article{BernoulliAFP,
author = {Lukas Bulwahn and Manuel Eberl},
title = {Bernoulli Numbers},
journal = {Archive of Formal Proofs},
month = jan,
year = 2017,
note = {\url{http://isaafp.org/entries/Bernoulli.shtml},
Formal proof development},
ISSN = {2150914x},
}
