Abstract

This entry provides Isabelle/HOl proofs for two important congruences involving Bernoulli numbers, namely Kummer’s congruence and Voronoi’s congruence. The proofs follow Cohen’s textbook Number Theory Volume II: Analytic and Modern Tools.

One application of these congruences is to prove that there are infinitely many irregular primes, which I formalised as well.

BibTeX

@article{Kummer_Congruence-AFP,
  author  = {Manuel Eberl},
  title   = {{K}ummer's congruence},
  journal = {Archive of Formal Proofs},
  month   = {March},
  year    = {2024},
  note    = {\url{https://isa-afp.org/entries/Kummer_Congruence.html},
             Formal proof development},
  ISSN    = {2150-914x},
}