Seminar-Tiefenstudium

Tiefenstudium für Seminarvorträge

Ein Seminarvortrag, der als Tiefenstudium eines Papers vorbereitet wird. Zunächst hilft der Agent dem Nutzer in einer interaktiven Diskussion – gestützt auf Belege – bei der Auswahl des Papers. Dann schreibt er das Paper als Digest um, in dem jede Behauptung ihren Verifikationsstatus trägt. Er wiederholt die Berechnungen mit einem Computeralgebrasystem (CAS), formalisiert die Logik in Lean und zeichnet auf, was er im Paper findet. Schließlich baut er aus dieser einzigen Quelle der Wahrheit die Vortragsmaterialien. Der Nutzer entscheidet; der Agent schlägt mit Belegen vor und prüft jede seiner Aussagen.

Gebündelte Dateien beziehen sich auf das Basisverzeichnis dieses Skills (wird beim Laden des Skills angezeigt); unten wird es als $SKILL bezeichnet. Projektdateien gehen in das Projektverzeichnis des Nutzers, niemals in $SKILL.

Phasen und was zu lesen ist

Phase	Zuerst lesen	Hinterlässt
0 Aufnahme	references/intake.md	Antworten in MEMORY.md, offene Entscheidungen in PLAN.md
1 Themenfindung	references/ideation.md	Das ausgewählte Paper; jeder Kandidat in JOURNAL.md
2 Quelle, Gerüst, Digest	references/digest.md	Repository, source/SOURCE.md, Digest mit Befundregister
3 Verifikation	references/verification.md, references/lean-palomar.md, references/compute.md	CAS-Transkripte, numerische Screenshots, Lean-Bibliothek, Audit, Logs
4 Materialien	references/materials.md, templates/briefs/	Notizen, Folien, Tafelplan, Verso-Dokument, Landingpage, Vault
5 Live-Demo	references/live-demo.md	Eine geprobte Demodatei und ein Fallback
6 Dokumentation	references/documentation.md	Journal, Plan, Gedächtnis, Vault-Notizen, Commits
7 Veröffentlichung	references/publishing.md	Nichts, es sei denn, der Nutzer fragt in dieser Sitzung danach
beliebig	references/traps.md	Vor Lean-, Cluster-, CAS- oder Site-Arbeit lesen
CS-Paper	references/computer-science.md	Die informatikspezifische Lesart der Phasen 1–5

Die Phasen sind ein Menü, kein Marschbefehl. Ein reiner Lesevortrag umfasst die Phasen 0–2 plus die benötigten Materialien; ein Nutzer, der bereits mit einem Paper kommt, beginnt mit Phase 0 und überspringt Phase 1.

Prinzipien

1. Der Nutzer wählt; Sie schlagen mit Belegen vor. Wählen Sie niemals das Paper, die Tiefe oder das Publikationsziel stillschweigend aus. Eine Umleitung („nicht überzeugt“, „etwas aktuelleres“) ist normal: Sie verfeinert das Profil. Beginnen Sie also eine neue Runde, anstatt die letzte zu verteidigen.
2. Nur Primärquellen. Überprüfen Sie Titel, Autoren, Daten, Version, Seitenzahl und Code-Verfügbarkeit an der Quelle: der arXiv-Abstract-Seite oder -API, dem PDF selbst, dem Repository. Kennzeichnen Sie Ankündigungen von Unternehmen oder der Presse als Behauptungen.
3. Jede gezeigte Zahl wird berechnet, niemals aus dem Gedächtnis zitiert. Zahlen auf Folien, Seiten und in den Notizen stammen aus ausgeführten Notebooks, CAS-Transkripten, Lean-Ausgaben oder Build-Logs.
4. Eine einzige Quelle der Wahrheit. Der Digest ist die mathematische Quelle der Wahrheit. Jede seiner Behauptungen ist mit [Lean], [CAS], [num], [exp] oder [paper] gekennzeichnet. Die Notizen, Folien, das Verso-Dokument und die Seite leiten sich daraus ab und widersprechen ihm niemals.
5. Das CAS findet, der Beweisassistent prüft. Zertifikate gehen von CAS-Transkripten über einen Generator (tools/cert2lean.py) nach Lean. Generierte Dateien werden neu gebaut, niemals von Hand bearbeitet.
6. Schwierige, aber Standard-Fakten werden zu expliziten Hypothesen, niemals zu Axiomen. Halten Sie jede im Digest und in den Formalisierungs-Metadaten fest.
7. Befunde sind standardmäßig vertraulich. Befunde über das unveröffentlichte Paper einer anderen Person bleiben im Projekt, bis der Nutzer entscheidet. Bei einem echten Fehler schlagen Sie vor, zuerst die Autoren zu informieren.
8. Schützen Sie die Maschine und gemeinsame Ressourcen. Überprüfen Sie den freien Speicherplatz, bevor Sie Toolchains installieren, führen Sie lake update niemals ohne MATHLIB_NO_CACHE_ON_UPDATE=1 aus und bauen Sie niemals innerhalb der anderen Projekte des Nutzers. Beachten Sie die Cluster-Etikette in references/compute.md.
9. Ein Besitzer pro Datei. Jeder Subagent schreibt nur in sein eigenes Verzeichnis; Sie integrieren, prüfen und committen.
10. Nach außen gerichtete Aktionen benötigen eine explizite Anfrage in der aktuellen Sitzung. Dies umfasst das Bereitstellen, Pushen, Erstellen eines entfernten Repositories und das Veröffentlichen eines Artefakts. Schreiben Sie niemals ein Geheimnis (Passwort, Token, privater Schlüssel) in eine Datei.
11. Suchen Sie zuerst im Jargon des Nutzers in dessen eigenen Dateien. Ein unbekannter Begriff („Registerklasse“, ein Seminarakronym) ist oft in ihren Notizen oder Projekten definiert. Suchen Sie dort, dann im Web, dann fragen Sie.

Phase 0: Aufnahme

Erheben Sie zuerst schreibgeschützt die Umgebungsdaten, damit die Fragen konkrete Optionen bieten. Überprüfen Sie den freien Speicherplatz (df -h ~), installierte Lean-Toolchains, das verfügbare CAS (lokal oder entfernt), Python und uv sowie alle Projekte, die der Nutzer als Format zum Kopieren genannt hat. Fragen Sie dann mit dem Fragetool (AskUserQuestion in Claude Code): höchstens vier Fragen pro Aufruf, zwei bis vier Optionen jeweils, die empfohlene Option zuerst und mit „(Empfohlen)“ markiert. Der Fragenkatalog befindet sich in references/intake.md; er umfasst den Vortrag, das Thema und die Tiefe, das CAS und die Berechnung, die Ergebnisse, wie das Dashboard bereitgestellt wird (nur lokal oder online und wo; jetzt oder später) und git. Überspringen Sie, was die erste Nachricht des Nutzers bereits beantwortet, und bestätigen Sie es in einer Zeile statt dessen. Zeichnen Sie Antworten als datierte Entscheidungen in MEMORY.md auf; offene Punkte kommen als ❓ in PLAN.md.

Phase 1: Themenfindung (wenn das Paper nicht vorgegeben ist)

Führen Sie Runden durch, bis der Nutzer auswählt (references/ideation.md):

1. Erstellen Sie ein Interessenprofil aus dem arXiv-Eintrag des Nutzers (tools/arxiv_scan.py author), den READMEs seiner aktuellen Projekte und dem, was er gesagt hat. Zeigen Sie es in drei Zeilen an, damit er es korrigieren kann.
2. Suchen Sie parallel: Websuche nach Neuigkeiten; die arXiv-API über Kategorien × Themen × ein Aktualitätsfenster (tools/arxiv_scan.py scan, dann rank); Code-Repositories über die GitHub-API und flache Klone im Scratchpad (tools/tactic_census.py für Lean-Code).
3. Überprüfen Sie jeden Kandidaten, den Sie präsentieren werden (ID, Titel, Autoren, Daten, Versionen, Seiten aus dem PDF, Code-Link). Überprüfen Sie eine spektakuläre Behauptung selbst dann, wenn das günstig ist.
4. Präsentieren Sie die Shortlist in Prosa: eine Empfehlung mit Begründung, warum sie zum Nutzer und zum Format passt, zwei oder drei Alternativen mit Vor- und Nachteilen, Papers knapp außerhalb der Filter, Nachrichten, die fünf Minuten wert sind, und die Quellen. Enden Sie mit einer direkten Frage. Das Fragetool dient der klaren endgültigen Auswahl; wenn der Nutzer es ablehnt, um zu klären, möchte er reden – fragen Sie, was er ändern möchte.
5. Protokollieren Sie jeden Kandidaten und den Grund, warum er verworfen wurde; dies kommt zum Zeitpunkt des Gerüstbaus in JOURNAL.md.

Phase 2: Quelle, Gerüst, Digest

Holen Sie das PDF und die LaTeX-Quelle in source/ (git-ignoriert). Zeichnen Sie die Version und die SHA-256-Prüfsummen in source/SOURCE.md auf. Transkribieren Sie Formeln und Listen aus dem LaTeX, niemals aus der PDF-Textschicht. Bauen Sie das Projektgerüst mit tools/scaffold.py (Dokumentationsvorlagen, den Digest und optional die Lean-, CAS-, Cluster-, Site-, Folien-, Buch-, Verso- und Vault-Skelette). Schreiben Sie dann den Digest (templates/digest/digest.md): das Ergebnis in drei Zeilen, Hintergrund, Aufbau, ein Abschnitt pro Theorem mit seiner Beweisarchitektur und Status-Tags, das Befundregister (Schweregrade: bestätigt / Formulierung / implizite Hypothese / Verschärfung / Fehler) und Übungen. Details: references/digest.md.

Phase 3: Verifikation

Wandeln Sie jede rechnerische Behauptung und jedes „man rechnet nach“ in eine Zeile einer Verifikationstabelle in PLAN.md um, und arbeiten Sie sie dann ab:

• numerische Screenshots zuerst (hohe Genauigkeit; sie fangen Transkriptionsfehler, sie beweisen nichts);
• CAS-Skripte mit festgehaltenen Transkripten, deren CHECK-Zeilen wahr sein müssen; Unstimmigkeiten gehen in das Befundregister (references/verification.md);
• Zertifikate: das CAS gibt CERT-Blöcke aus, tools/cert2lean.py schreibt die Lean-Datei, und linear_combination oder ring prüft jede Identität; grind kann dieselben Schritte ohne Zertifikat erneut beweisen, was es wert ist, gezeigt zu werden;
• Lean: zuerst die Aussagen, dann die Beweise; leicht oder Palomar-Klasse (Challenge.lean/Solution.lean/comparator.json, nur Standard-Axiome, Axiom-Audit mit import all, lake comparator --paranoid, warnungsfreier Build, Logs). Siehe references/lean-palomar.md und references/compute.md für lokale vs. Cluster-Builds und die Speicherplatz-Regeln.

Behandeln Sie Linter-Warnungen als mögliche Befunde: Ein ungenutztes Instanzargument kann bedeuten, dass der Satz allgemeiner gilt als im Paper angegeben.

Phase 4: Materialien, durch parallele Subagenten

Starten Sie einen Hintergrundagenten pro Ergebnis, jeder besitzt sein Verzeichnis: CAS-Neuverifikation, das Verso-Dokument, Notizen (Jupyter Book), Folien mit Tafelplan, und die Landingpage mit ihrem Hero-Bild und dem Vault. Füllen Sie die Briefings in templates/briefs/. Jedes Briefing nennt die Quellen der Wahrheit (den Digest, die Lean-Dateien, die Transkripte), die Fakten, die es angeben darf, die Befehle, die es ausführen darf, und dass es niemals Zahlen, Namen, Zeiten oder Räume erfinden darf. Fahren Sie während ihrer Ausführung mit der Verifikation fort. Wenn sich ein Fakt ändert (ein neues Ergebnis, eine neue Zählung, eine neue Demo), senden Sie jedem laufenden Agenten eine kurze, in sich geschlossene Aktualisierung mit SendMessage: was sich geändert hat, wo es zu finden ist, was hinzugefügt werden soll, „optional, behalten Sie Ihren aktuellen Plan bei“. Agenten leiten Zahlen neu her, also überprüfen sie auch den Digest: Bitten Sie sie, jede Unstimmigkeit zu melden, korrigieren Sie dann den Digest (mit Datum) und informieren Sie die anderen. Beobachten Sie den freien Speicher, während mehrere Agenten laufen. Wenn ein Agent fertig ist, überprüfen Sie seine Ausgabe (bauen Sie sie, öffnen Sie sie, machen Sie Headless-Screenshots), verlinken Sie die Ergebnisse miteinander und committen Sie. Generierte Materialien werden aus ihren Quellen neu erstellt: Die Folien lehnen Code ab, der kein wörtlicher Auszug ist, und sie enthalten ausgelagerte Bibliotheken, damit der Vortrag offline funktioniert. Details: references/materials.md.

Phase 5: Live-Demo

Erstellen Sie eine Demodatei, die in Sekunden läuft: #check und #print axioms des Hauptsatzes, ein durch linear_combination geprüftes Zertifikat, derselbe Fakt bewiesen durch grind und eine auskommentierte „Zerstören“-Variante, die sichtbar fehlschlägt. Führen Sie sie lokal oder remote über den demo-Befehl des Cluster-Treibers aus. Probieren Sie sie zweimal und halten Sie einen Fallback bereit (das gerenderte Verso-Dokument oder Screenshots). Details: references/live-demo.md.

Phase 6: Dokumentation und Ende der Sitzung

Das Projekt enthält CLAUDE.md (Betriebsanleitung), MEMORY.md (datierte Fakten und Entscheidungen), JOURNAL.md (datierte Einträge), PLAN.md (✅ erledigt · 🟡 in Arbeit · ⬜ zu erledigen · ❓ Entscheidung des Nutzers), MAINTENANCE.md (Runbook), README.md und den Vault. Am Ende jeder Sitzung: einen Journaleintrag anhängen, den Plan aktualisieren, Vault-Notizen für neue Konzepte und Entscheidungen hinzufügen und committen (Conventional Commits). Client-Gedächtnisdateien enthalten nur Fakten, die das Projekt überdauern sollten. Details: references/documentation.md.

Phase 7: Veröffentlichung (nur auf ausdrückliche Anfrage)

Bauen Sie alles zuerst lokal. Veröffentlichen Sie nur, was der Nutzer in dieser Sitzung verlangt hat, am in Phase 0 gewählten Ziel: ein privates Claude-Artefakt, GitHub Pages oder einen Webserver über ein Whitelist-Deploy-Skript mit einem Trockenlauf, einem Link-Check und einem Leck-Scan (tools/leak_scan.py). Ein öffentliches Repository erhält eine neue Historie und einen Leck-Scan, bevor der Nutzer es pusht. Details: references/publishing.md.

Start-Checkliste

1. Fragen aus Phase 0 beantwortet, Entscheidungen aufgezeichnet.
2. Paper ausgewählt (Phase 1) oder vorgegeben; Quelle geholt und gechecmsumt.
3. python3 "$SKILL/tools/scaffold.py" <Projekt> ...; git init; erster Commit.
4. Digest geschrieben, Behauptungen getaggt, Verifikationstabelle in PLAN.md.
5. Verifikation und Formalisierung gestartet; Material-Agenten gestartet, sobald der Digest stabil ist.
6. Ende der Sitzung: Journal, Plan, Vault, Commit.