Algebra in Lean

A hands-on introduction to formalizing algebra with the proof assistant Lean and its mathematical library Mathlib. The course accompanies the lecture notes Algebra und Zahlentheorie (Stefan Kebekus, Universität Freiburg) and is aimed at students who are learning algebra and have little prior experience with Lean.

Selected proofs from the lecture notes are translated into Lean sentence by sentence: the German original of each sentence is quoted as a comment directly above the Lean code implementing it, so you can see how the standard phrases of a lecture-style proof translate into Lean/Mathlib.

Getting started

1. Install Lean (elan, VS Code and the Lean 4 extension).

2. Clone this repository and fetch the precompiled Mathlib cache:

   git clone <repository url>
   cd AlgebraInLean
   lake exe cache get
   

3. Open the folder in VS Code and start with AlgebraInLean/LittleFermat.lean.

Contents

File	Lecture notes	Topic
AlgebraInLean/LittleFermat.lean	Kapitel 17	Fermat's little theorem via Lagrange
AlgebraInLean/Cauchy.lean	Kapitel 18	The key lemma on fixed points and Cauchy's theorem

License

CC-BY 4.0, like the lecture notes.