### Abstract

Bernoulli numbers were first discovered in the closed-form expansion of the sum 1m + 2m + … + nm 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, and some advanced facts like their relationship to the Riemann zeta function on positive even integers.

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 log-Gamma function) and prove their basic properties.

### License

BSD License

### Topics

- Mathematics/Analysis
- Mathematics/Number theory

### Session Bernoulli

- Bernoulli
- Periodic_Bernpoly
- Bernoulli_FPS
- Bernoulli_Zeta

### Used by

- Khovanskii's Theorem
- The Lambert W Function on the Reals
- The Hurwitz and Riemann ζ Functions
- The Euler–MacLaurin Formula
- Stirling’s formula

## Cite

×

Bernoulli-AFP

    @article{Bernoulli-AFP,
      author  = {Lukas Bulwahn and Manuel Eberl},
      title   = {Bernoulli Numbers},
      journal = {Archive of Formal Proofs},
      month   = {January},
      year    = {2017},
      note    = {\url{https://isa-afp.org/entries/Bernoulli.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Dec 14, 2021 : Isabelle2021-1
- Feb 23, 2021 : Isabelle2021
- Apr 18, 2020 : Isabelle2020
- Jun 11, 2019 : Isabelle2019
- Aug 16, 2018 : Isabelle2018
- Oct 10, 2017 : Isabelle2017
- Jan 24, 2017 : Isabelle2016-1