DROPS

Document

DOI: 10.4230/LIPIcs.ITP.2023.22

Group Cohomology in the Lean Community Library

Authors: Amelia Livingston

Published in: LIPIcs, Volume 268, 14th International Conference on Interactive Theorem Proving (ITP 2023)

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.

Cite as

Amelia Livingston. Group Cohomology in the Lean Community Library. In 14th International Conference on Interactive Theorem Proving (ITP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 268, pp. 22:1-22:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@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/entities/document/10.4230/LIPIcs.ITP.2023.22},
  URN =		{urn:nbn:de:0030-drops-183974},
  doi =		{10.4230/LIPIcs.ITP.2023.22},
  annote =	{Keywords: formal math, Lean, mathlib, group cohomology, homological algebra}
}

Search Results

Documents authored by Livingston, Amelia

Group Cohomology in the Lean Community Library

Abstract

Cite as

Thanks for your feedback!

Could not send message