2026-08-10T23:04:15Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:18397 2024-03-06T11:01:47Z ddc:004 open_access

Group Cohomology in the Lean Community Library Livingston, Amelia formal math Lean mathlib group cohomology homological algebra Group cohomology is a tool which has become indispensable in a wide range of modern mathematics, like algebraic geometry and algebraic number theory, as well as group theory itself. For example, it allows us to reformulate classical class field theory in cohomological terms; this formulation is essential to landmarks of modern number theory, like Wiles’s proof of Fermat’s Last Theorem. We explore the challenges of formalising group cohomology in the Lean theorem prover in a generality suitable for inclusion in the community library mathlib. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Amelia Livingston 2023 Is Part Of LIPIcs, Volume 268, 14th International Conference on Interactive Theorem Proving (ITP 2023) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.ITP.2023.22 urn:nbn:de:0030-drops-183974 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2023.22 eng https://creativecommons.org/licenses/by/4.0/legalcode