Group cohomology, a central tool in algebra and number theory, lacked a machine-checked formalization in Lean's mathlib library. Both the abstract derived-functor construction and the concrete cochain complex computing it needed to be formalized with appropriate API design for a large-scale library.

The paper describes the formalization of group cohomology in mathlib as derived functors of the invariants functor, along with the explicit cochain complex computing it and the long exact sequence in cohomology. The work addresses API design challenges for making the formalization reusable within a large library ecosystem.

Group cohomology is formalized and contributed to mathlib, covering the derived-functor definition, the explicit cochain complex, and the long exact sequence. The paper provides API design insights relevant to other large-scale formalization efforts.