License: 
Creative Commons Attribution 4.0 International license (CC BY 4.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.ITP.2023.22
URN: urn:nbn:de:0030-drops-183974
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2023/18397/
Livingston, Amelia
Group Cohomology in the Lean Community Library
Abstract
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.
BibTeX - Entry
@InProceedings{livingston:LIPIcs.ITP.2023.22,
author = {Livingston, Amelia},
title = {{Group Cohomology in the Lean Community Library}},
booktitle = {14th International Conference on Interactive Theorem Proving (ITP 2023)},
pages = {22:1--22:17},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-284-6},
ISSN = {1868-8969},
year = {2023},
volume = {268},
editor = {Naumowicz, Adam and Thiemann, Ren\'{e}},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/opus/volltexte/2023/18397},
URN = {urn:nbn:de:0030-drops-183974},
doi = {10.4230/LIPIcs.ITP.2023.22},
annote = {Keywords: formal math, Lean, mathlib, group cohomology, homological algebra}
}
|
Keywords: |
|
formal math, Lean, mathlib, group cohomology, homological algebra |
|
Collection: |
|
14th International Conference on Interactive Theorem Proving (ITP 2023) |
|
Issue Date: |
|
2023 |
|
Date of publication: |
|
26.07.2023 |
