CLAUDE.md

This file provides guidance to Claude Code (claude.ai/code) when working with code in this repository.

Was das Repository ist

Kursnotizen „Algebra in Lean“ zur Vorlesung Algebra und Zahlentheorie (Stefan Kebekus, Universität Freiburg). Ausgewählte Beweise des Skripts werden Satz für Satz nach Lean 4 / Mathlib übersetzt: der deutsche Originalsatz steht als Zitat bzw. Kommentar direkt über dem Lean-Code. Jedes Kapitel endet mit einer Übungsaufgabe, deren sorry die Studierenden ersetzen sollen.

Die Prosa ist deutsch. Kommentare, Aufgabentexte und Kapitelnamen auf Deutsch schreiben; Lemma- und Theoremnamen ebenfalls deutsch (neutral_eindeutig, gradformel).

Befehle

lake exe cache get                       # Mathlib-Cache holen (vor dem ersten Build!)
lake build                               # Übungsdateien + Buch elaborieren
lake exe algebrainlean --output _out     # Buch nach _out/html-multi rendern
python3 -m http.server 8000 -d _out/html-multi
./deploy.sh                              # baut und rsynct nach cplx.vm.uni-freiburg.de

Einzelne Datei prüfen: lake build AlgebraInLean.Degrees bzw. lake build Book.Degrees. Es gibt keine Testsuite — „Test“ heißt: lake build läuft ohne Fehler durch. Fehlende Beweise sind absichtliche sorrys (Warnung, kein Fehler).

Doppelstruktur: `AlgebraInLean/` ↔ `Book/`

Jedes Kapitel existiert zweimal, mit demselben Dateinamen:

AlgebraInLean/X.lean — die Übungsdatei, die Studierende in VS Code öffnen. import Mathlib (bequem), namespace AlgebraInLean, Prosa in /-! … -/.
Book/X.lean — dasselbe Material als Verso-Kapitel. Prosa als Verso-Markup, Lean-Code in ```lean-Blöcken, die beim Build mitelaboriert werden — die gerenderten Beweise kompilieren also garantiert.

Wer Mathematik ändert, muss beide Seiten anfassen; sie driften sonst auseinander. Neue Kapitel zusätzlich in AlgebraInLean.lean (Import) und Book.lean (Import + {include 0 Book.X}) eintragen, und die Tabelle in README.md ergänzen. Achtung: Eine Übungsdatei, die nicht in AlgebraInLean.lean importiert ist, wird von lake build gar nicht kompiliert — sie kann also unbemerkt kaputt sein.

Konventionen in Book/:

Kopf jeder Datei: import VersoManual, import Manual.Meta, dann Minimal-Imports von Mathlib (mit #min_imports ermittelt) statt import Mathlib — das hält den Buch-Build erträglich schnell.
set_option pp.rawOnError true und set_option verso.docstring.allowMissing true.
#doc (Manual) "Titel" => mit %%%-Block: htmlSplit := .never, tag/file als deutscher URL-Slug (gradformel, reziprozitaet, …). file bestimmt den Pfad in _out/html-multi/; Slugs nicht nachträglich ändern, sonst brechen Links auf dem Server.
Mathe im Verso-Dialekt: $…inline, $$… `` abgesetzt.
Skript-Zitate als Blockquotes (>); Folgezeilen ohne > werden per Lazy Continuation fortgesetzt, müssen aber eingerückt sein.
open- und variable-Deklarationen gelten über Codeblöcke hinweg für das ganze Kapitel.
In Kapiteln, die Polynomial öffnen, nur open Verso.Genre schreiben, nie open Verso.Genre Manual — sonst ist C doppeldeutig (Manual.C vs. Polynomial.C).
Verso warnt bei Codezeilen über 60 Spalten (verso.code.warnLineLength); Lean-Code entsprechend umbrechen. Die Warnungen stehen in der vollen Build-Ausgabe — nicht durch tail pipen, sondern nach too long greppen.

Kapitelaufbau

Bewährte Gliederung eines Buchkapitels (an bestehenden Kapiteln orientieren, z. B. Book/Elements.lean):

Einleitung mit Bezug zum Skript (Satznummer!).
# Das Mathlib-Wörterbuch — Begriffe des Skripts ↔ Mathlib-Namen. Nicht duplizieren: Folgekapitel verweisen auf das Wörterbuch des Vorkapitels.
Hauptsatz mit kurzem Beweis, der die Mathlib-Lemmata ehrlich zitiert („der gesamte Rest des Beweises ist das Lemma …“).
# Übungsaufgabe — genau ein sorry; im Text den Pfad der zugehörigen Übungsdatei nennen. Die Musterlösung vor dem Einchecken separat verifizieren (in einer Scratch-Datei kompilieren), dann wieder durch sorry ersetzen.
# Der vollständige Beweis — der Skript-Beweis Satz für Satz, jeder deutsche Originalsatz als Kommentar über dem Lean-Code.

Arbeitsweise für neue Beweise

Erst in einer Scratch-Datei (außerhalb des Repos) mit import Mathlib prototypen, bis alles kompiliert; dann mit #min_imports die Minimal-Imports fürs Buchkapitel bestimmen und dort einpflegen. Kapitel-Builds dauern damit Sekunden statt Minuten.
Nach dem Deploy die Live-Seite prüfen (z. B. curl auf <title>).

Verzahnung mit dem Skript

Das LaTeX-Skript liegt in ../AlgebraZahlentheorie. Dort verlinkt das Makro \leanlink{slug} auf https://cplx.vm.uni-freiburg.de/storage/algebra-in-lean/<slug>/ — der file-Slug eines Kapitels ist also Teil der Schnittstelle. Neues Kapitel ⇒ ggf. \leanlink an der passenden Stelle im Skript setzen.
Skript-Labels (satz:3-5-4, kor:TdA, …) stimmen nicht immer mit den gedruckten Nummern überein; verbindlich ist ../AlgebraZahlentheorie/AlgebraZahlentheorie.aux.

Build-Setup

Toolchain in lean-toolchain ist verbindlich (v4.33.0-rc2).
lakefile.lean: Reihenfolge der requires ist bewusst — verso-manual (aus dem Lean-Reference-Manual-Repo, das seinerseits die passende Verso-Nightly pinnt) vor Mathlib, damit Mathlibs Pins der geteilten Abhängigkeiten gewinnen; sonst verweigert lake exe cache get den Dienst. Verso wird nicht direkt required.
Main.lean konfiguriert die Ausgabe: nur Multi-Page-HTML, kein TeX, eigene CSS/JS aus static/ (Theme folgt Pfaffelhubers leancourse). KaTeX bringt Verso selbst mit — keine zweite Kopie einbinden, sonst wird jede Formel doppelt gerendert.
.lake/, _out/ und public/ sind nicht versioniert; public/ ist die ausgelieferte Kopie der Build-Ausgabe.

6.0 KiB Raw Permalink Blame History