9. Infinitely many irregular primes
This chapter records the Carlitz route from Kummer congruences to the infinitude of
irregular primes. The theorem proved in Lean is that
\{p : \mathbb{N} \mid p\text{ is prime and }p\text{ is not regular}\} is infinite.
The proof is by finite-set escape: given a finite set S of candidate irregular
primes, construct a new prime p\notin S dividing the numerator of a suitable
divided Bernoulli number B_M/M, then use Kummer congruences and Kummer's criterion
to show that p is irregular.