Kummer's criterion formalized in Lean

Together with Chris Birkbeck, we formalized (using LLMs) Kummer’s criterion for regularity. See the repository.