Minor update
This commit is contained in:
Stefan Kebekus committed
1 parent
484caeea98
commit
a4ece61abe
3 files changed
+263
-239
No files matched your search
@@ -24,3 +24,9 @@ __pycache__
|
||||
/corpus
|
||||
/tools/corpus/registry.json
|
||||
/tools/corpus/systemprompt-erklaeren-komplett.md
|
||||
|
||||
# NotebookLM-Quellen: Volltexte und Verzeichnisse sind aus corpus/ abgeleitet,
|
||||
# die handgeschriebenen Dossiers und die README bleiben im Repository.
|
||||
/notebooklm/*-volltext.md
|
||||
/notebooklm/00-inhaltsverzeichnis.md
|
||||
/notebooklm/00-verzeichnis-aussagen-kompakt.md
|
||||
Vendored
+217
-213
@@ -1,223 +1,227 @@
|
||||
konstruierbaren
|
||||
Ecks
|
||||
konstruierbar
|
||||
Arnol
|
||||
Maulschellen
|
||||
Duerer
|
||||
Halbierungspunkt
|
||||
Viertelungspunkt-Halbierungspunkt
|
||||
inkommensurabel
|
||||
Sekantenlänge
|
||||
Sickinger
|
||||
Serge
|
||||
CoCalc
|
||||
Dava
|
||||
Sobel
|
||||
Permutationsgruppe
|
||||
Zerfällungskörper
|
||||
Galoisgruppe
|
||||
Picard-Lindelöf
|
||||
Lie
|
||||
Nordfjordeid
|
||||
Kristiania
|
||||
Zerfällungskörpers
|
||||
Sophus
|
||||
Beaumont-en-Auge
|
||||
Liesche
|
||||
Inversenbildung
|
||||
Beutelspacher
|
||||
Erklärvideo
|
||||
nullteilerfrei
|
||||
nullteilerfreien
|
||||
Transzendenzbeweis
|
||||
Lorettoberg
|
||||
Normiertheit
|
||||
hinzuadjungieren
|
||||
Algebraizität
|
||||
Gerolamo
|
||||
Cardano
|
||||
Girolamo
|
||||
Cardanus
|
||||
Mediolanensis
|
||||
Cardan
|
||||
Nicolo
|
||||
Tartaglia
|
||||
Scipione
|
||||
del
|
||||
Ferro
|
||||
Radikalerweiterung
|
||||
Teilbarkeitsfragen
|
||||
Polynom-
|
||||
Teilbarkeitsüberlegungen
|
||||
schrecklicherweise
|
||||
Teilerkette
|
||||
Teilerkettensatz
|
||||
Bryn
|
||||
Mawr
|
||||
prim
|
||||
faktoriell
|
||||
UFD
|
||||
faktorieller
|
||||
Repräsentantensystem
|
||||
Teilbarkeitseigenschaften
|
||||
kgV
|
||||
faktoriellen
|
||||
Geodät
|
||||
Quotientenkörper
|
||||
Quotientenkörpers
|
||||
Irreduzibilitätskriterien
|
||||
Irreduzibilitätskriterium
|
||||
Teilbarkeitsbetrachtungen
|
||||
Teilerpolynome
|
||||
Lodovico
|
||||
Lagrangia
|
||||
Interpolationsformel
|
||||
Schönemann
|
||||
Driesen
|
||||
Friedebergischer
|
||||
reduzibel
|
||||
Einsetzungskomposition
|
||||
Substitutionsmorphismus
|
||||
Konstruierbarkeitsfragen
|
||||
konjungierte
|
||||
konstruierbare
|
||||
Konstruierbarkeitsfrage
|
||||
transzendent
|
||||
Rechtsideale
|
||||
Sorau
|
||||
Dedekind
|
||||
nicht-faktoriellen
|
||||
Hauptideale
|
||||
Erzeugendensysteme
|
||||
Gödelschen
|
||||
Erzeugendensystems
|
||||
Erzeugendensystem
|
||||
Teiler-
|
||||
Hauptidealen
|
||||
Faktorialität
|
||||
Quotientenvektoraumes
|
||||
Quotientenvektorräumen
|
||||
Quotientenvektorräume
|
||||
Quotientenring
|
||||
Repräsentantensystems
|
||||
Homomorphiesatzes
|
||||
Homomorphiesatz
|
||||
Quotientenabbildung
|
||||
Urbildmenge
|
||||
Primideale
|
||||
Primideals
|
||||
Primideal
|
||||
Summenideal
|
||||
Teilerfremdheit
|
||||
Funktionenkörper
|
||||
Kodierungstheorie
|
||||
Substitutionsabbildung
|
||||
Steinitz
|
||||
Laurahütte
|
||||
nicht-Kanonizität
|
||||
Zerfällungskörpern
|
||||
inseparable
|
||||
Teilbarkeitsrelationen
|
||||
Frobenius-Morphismus
|
||||
Frobenius-Endomorphismus
|
||||
Einselements
|
||||
separabel
|
||||
inseparabel
|
||||
Separabilität
|
||||
Substitutionsmorphismen
|
||||
Separabilitätsgrad
|
||||
inseparablen
|
||||
Galoiserweiterung
|
||||
Quotientengruppe
|
||||
Galoisgruppen
|
||||
Signumsabbildung
|
||||
Kleinsche
|
||||
Primzahlordnung
|
||||
Klassifikationssatzes
|
||||
Klassifikationsprogramms
|
||||
Solomon
|
||||
Gorenstein
|
||||
.ten
|
||||
.ter
|
||||
.te
|
||||
.tes
|
||||
Primteiler
|
||||
Galoisch
|
||||
Fermatsche
|
||||
Fermatzahl
|
||||
Bunsenstraße
|
||||
Courant
|
||||
Foliaten
|
||||
Koeffizientenschemata
|
||||
Gauss
|
||||
MSRI
|
||||
Galoissche
|
||||
Bourg-la-Reine
|
||||
quadratfreie
|
||||
Évariste
|
||||
Galoisschen
|
||||
Galoiserweiterungen
|
||||
Konjugation
|
||||
galoiskonjugierten
|
||||
Nichtkonstruierbarkeitsbeweisen
|
||||
Nichtkonstruierbarkeitsbeweise
|
||||
Fixkörper
|
||||
Äquivalenzklassen
|
||||
Arnol
|
||||
Artin
|
||||
Automorphismengruppe
|
||||
Frobeniusmorphismus
|
||||
Fixkörperkonstruktion
|
||||
Äquivalenzklassen
|
||||
Sylow
|
||||
Primzahlpotenzteiler
|
||||
Christiania
|
||||
Cauchy
|
||||
Bahnengleichung
|
||||
Bahnenraum
|
||||
Beaumont-de-Lomagne
|
||||
Beaumont-en-Auge
|
||||
Beutelspacher
|
||||
Beutelspachers
|
||||
Bloomington
|
||||
Bourg-la-Reine
|
||||
Bryn
|
||||
Building
|
||||
Bunsenstraße
|
||||
Camille
|
||||
Cardan
|
||||
Cardano
|
||||
Cardanus
|
||||
Castres
|
||||
Cauchy
|
||||
Christiania
|
||||
CoCalc
|
||||
Courant
|
||||
Dava
|
||||
Dedekind
|
||||
del
|
||||
Département
|
||||
Diedergruppe
|
||||
Driesen
|
||||
Duerer
|
||||
Ecks
|
||||
Einselements
|
||||
Einsetzungskomposition
|
||||
Erklärvideo
|
||||
Erzeugendensystem
|
||||
Erzeugendensysteme
|
||||
Erzeugendensystems
|
||||
Eulerus
|
||||
Évariste
|
||||
Faktorialität
|
||||
faktoriell
|
||||
faktoriellen
|
||||
faktorieller
|
||||
Feb
|
||||
Fermatsche
|
||||
Fermatzahl
|
||||
Ferro
|
||||
Fields-Medaillengewinner
|
||||
Fixkörper
|
||||
Fixkörperkonstruktion
|
||||
Foliaten
|
||||
Friedebergischer
|
||||
Frobenius-Endomorphismus
|
||||
Frobeniusmorphismus
|
||||
Frobenius-Morphismus
|
||||
Funktionenkörper
|
||||
Galoisch
|
||||
Galoiserweiterung
|
||||
Galoiserweiterungen
|
||||
Galoisgruppe
|
||||
Galoisgruppen
|
||||
galoiskonjugierten
|
||||
Galoissche
|
||||
Galoisschen
|
||||
Gauss
|
||||
Geodät
|
||||
Gerolamo
|
||||
Girolamo
|
||||
Gödelschen
|
||||
Gorenstein
|
||||
Gradformel
|
||||
Halbierungspunkt
|
||||
Hartnetts
|
||||
Hauptideale
|
||||
Hauptidealen
|
||||
Helsingfors
|
||||
hinzuadjungieren
|
||||
Homomorphiesatz
|
||||
Homomorphiesatzes
|
||||
Identifikationen
|
||||
indexerhaltend
|
||||
inklusionsumkehrend
|
||||
inkommensurabel
|
||||
inseparabel
|
||||
inseparable
|
||||
inseparablen
|
||||
Interpolationsformel
|
||||
Inversenbildung
|
||||
Irreduzibilitätskriterien
|
||||
Irreduzibilitätskriterium
|
||||
Isotropiegruppe
|
||||
kgV
|
||||
Klassifikationsprogramms
|
||||
Klassifikationssatzes
|
||||
Kleinsche
|
||||
Kodierungstheorie
|
||||
Koeffizientenschemata
|
||||
Konjugation
|
||||
konjungierte
|
||||
konstruierbar
|
||||
konstruierbare
|
||||
konstruierbaren
|
||||
Konstruierbarkeitsfrage
|
||||
Konstruierbarkeitsfragen
|
||||
Kristiania
|
||||
Lagrangia
|
||||
Laurahütte
|
||||
Lean
|
||||
LeanDex
|
||||
LeanExplore
|
||||
Legendre-Symbol
|
||||
Legendre-Symbole
|
||||
Legendre-Symbolen
|
||||
Leonhardus
|
||||
Lie
|
||||
Liesche
|
||||
Lodovico
|
||||
Loogle
|
||||
Lorettoberg
|
||||
Mathlib
|
||||
Mathlib-Deklarationen
|
||||
Mathlib-Dokumentation
|
||||
Maulschellen
|
||||
Mawr
|
||||
Mediolanensis
|
||||
Moduln
|
||||
MSRI
|
||||
nicht-faktoriellen
|
||||
nicht-Kanonizität
|
||||
Nichtkonstruierbarkeitsbeweise
|
||||
Nichtkonstruierbarkeitsbeweisen
|
||||
Nicolo
|
||||
Nordfjordeid
|
||||
Normalisator
|
||||
Normiertheit
|
||||
nullteilerfrei
|
||||
nullteilerfreien
|
||||
Peano-Axiomen
|
||||
Permutationsgruppe
|
||||
Picard-Lindelöf
|
||||
Polynom-
|
||||
prim
|
||||
Primideal
|
||||
Primideale
|
||||
Primideals
|
||||
Primteiler
|
||||
Primzahlordnung
|
||||
Primzahlpotenzteiler
|
||||
quadratfreie
|
||||
Quotientenabbildung
|
||||
Quotientengruppe
|
||||
Quotientenkörper
|
||||
Quotientenkörpers
|
||||
Quotientenring
|
||||
Quotientenvektoraumes
|
||||
Quotientenvektorraum
|
||||
Quotientenvektorräume
|
||||
Quotientenvektorräumen
|
||||
Radikalerweiterung
|
||||
Radikalerweiterungen
|
||||
Rechtsideale
|
||||
reduzibel
|
||||
Repräsentantenniveau
|
||||
Repräsentantensystem
|
||||
Repräsentantensystems
|
||||
Sceaux
|
||||
Scholze
|
||||
Schönemann
|
||||
schrecklicherweise
|
||||
Scipione
|
||||
Sekantenlänge
|
||||
separabel
|
||||
Separabilität
|
||||
Separabilitätsgrad
|
||||
Serge
|
||||
Sickinger
|
||||
Signumsabbildung
|
||||
Signums-Abbildung
|
||||
Sobel
|
||||
Solomon
|
||||
Sophus
|
||||
Sorau
|
||||
Stabilisatorgruppen
|
||||
Steinitz
|
||||
Substitutionsabbildung
|
||||
Substitutionsmorphismen
|
||||
Substitutionsmorphismus
|
||||
Summationsreihenfolge
|
||||
Summenideal
|
||||
Sylow
|
||||
Sylow-Satz
|
||||
Sylowuntergruppe
|
||||
Sylowuntergruppen
|
||||
Normalisator
|
||||
Camille
|
||||
Zykel
|
||||
Signums-Abbildung
|
||||
Sylow-Satz
|
||||
Isotropiegruppe
|
||||
Moduln
|
||||
Torsionsanteil
|
||||
Feb
|
||||
Radikalerweiterungen
|
||||
Gradformel
|
||||
Legendre-Symbol
|
||||
Repräsentantenniveau
|
||||
Identifikationen
|
||||
Legendre-Symbole
|
||||
Summationsreihenfolge
|
||||
Legendre-Symbolen
|
||||
uninspirierend
|
||||
Zornschen
|
||||
Bloomington
|
||||
Helsingfors
|
||||
Bahnenraum
|
||||
Stabilisatorgruppen
|
||||
Zentralisator
|
||||
Untergruppen
|
||||
Leonhardus
|
||||
Eulerus
|
||||
Diedergruppe
|
||||
Beaumont-de-Lomagne
|
||||
Département
|
||||
Tarn-et-Garonne
|
||||
Castres
|
||||
inklusionsumkehrend
|
||||
indexerhaltend
|
||||
Beutelspachers
|
||||
Quotientenvektorraum
|
||||
Lean
|
||||
Mathlib
|
||||
Mathlib-Dokumentation
|
||||
Scholze
|
||||
Tartaglia
|
||||
.te
|
||||
Teilbarkeitsbetrachtungen
|
||||
Teilbarkeitseigenschaften
|
||||
Teilbarkeitsfragen
|
||||
Teilbarkeitsrelationen
|
||||
Teilbarkeitsüberlegungen
|
||||
Teiler-
|
||||
Teilerfremdheit
|
||||
Teilerkette
|
||||
Teilerkettensatz
|
||||
Teilerpolynome
|
||||
.ten
|
||||
.ter
|
||||
Terence
|
||||
Hartnetts
|
||||
Building
|
||||
Fields-Medaillengewinner
|
||||
Peano-Axiomen
|
||||
.tes
|
||||
Torsionsanteil
|
||||
transzendent
|
||||
Transzendenzbeweis
|
||||
UFD
|
||||
uninspirierend
|
||||
Untergruppen
|
||||
Urbildmenge
|
||||
Viertelungspunkt-Halbierungspunkt
|
||||
Vorlesungsbeweis
|
||||
Zentralisator
|
||||
Zerfällungskörper
|
||||
Zerfällungskörpern
|
||||
Zerfällungskörpers
|
||||
Zornschen
|
||||
Zykel
|
||||
@@ -83,34 +83,48 @@ Mathlib-Dokumentation zeigt. Klicken Sie ruhig einmal darauf und vergleichen
|
||||
Sie: Dort steht genau das, was wir in der Vorlesung tun -- nur in einer
|
||||
Sprache, die auch ein Computer versteht.
|
||||
|
||||
Wenn Sie selbst erleben möchten, wie sich Beweisen mit dem Computer anfühlt,
|
||||
dann werfen Sie einen Blick in das Begleitskript
|
||||
\href{https://cplx.vm.uni-freiburg.de/storage/algebra-in-lean/}{„Algebra in
|
||||
Lean“}. Dort übersetzen wir ausgewählte Beweise aus diesem Skript Satz für
|
||||
Satz in Lean; über jedem Stück Code steht dabei der deutsche Originalsatz,
|
||||
sodass Sie genau verfolgen können, wie aus einem Vorlesungsbeweis ein formaler
|
||||
Beweis wird. Programmiererfahrung brauchen Sie dafür nicht. Links mit der
|
||||
Beschriftung „\textsf{Algebra in Lean}“ führen aus diesem Skript jeweils
|
||||
direkt zum passenden Kapitel des Begleitskripts. Aber seien Sie gewarnt:
|
||||
Beweisen mit Lean fühlt sich an wie ein Computerspiel und kann süchtig machen!
|
||||
Wenn Sie das gleich ausprobieren möchten: Das
|
||||
\href{https://adam.math.hhu.de/\#/g/leanprover-community/NNG4}{„Natural Number
|
||||
Game“}\index{Natural Number Game} läuft direkt im Browser, ganz ohne
|
||||
Installation. Dort bauen Sie die Arithmetik der natürlichen Zahlen aus den
|
||||
Peano-Axiomen auf -- von $2+2=4$ bis zu den Potenzgesetzen -- und lernen dabei
|
||||
spielerisch die wichtigsten Beweistechniken von Lean. Kaum jemand hört
|
||||
freiwillig auf, bevor das letzte Level gelöst ist.
|
||||
|
||||
Die Geschichte von Lean und Mathlib ist mehrfach spannend erzählt worden; die
|
||||
vorliegende Kurzdarstellung stützt sich unter anderem auf die folgenden Texte.
|
||||
Kevin Hartnetts Artikel „Building the Mathematical Library of the Future“
|
||||
Die Geschichte von Lean und Mathlib ist mehrfach spannend erzählt worden. Kevin
|
||||
Hartnetts Artikel „Building the Mathematical Library of the Future“
|
||||
\cite{Hartnett20} beschreibt, wie die Mathlib entstanden ist; in
|
||||
\cite{Hartnett21} berichtet derselbe Autor, wie Lean erstmals ein Resultat an
|
||||
vorderster Front der Forschung -- einen Beweis von Peter Scholze --
|
||||
verifiziert hat, und sein Buch \cite{Hartnett26} erzählt die ganze Geschichte
|
||||
ausführlich. Die Simons Foundation, die die Entwicklung von Lean maßgeblich
|
||||
finanziert, beschreibt in \cite{Duong26}, wie Lean das Vertrauen in
|
||||
mathematische Ergebnisse auf eine neue Grundlage stellt.
|
||||
vorderster Front der Forschung -- einen Beweis von Peter Scholze -- verifiziert
|
||||
hat, und sein Buch \cite{Hartnett26} erzählt die ganze Geschichte ausführlich.
|
||||
Die Simons Foundation, die die Entwicklung von Lean maßgeblich finanziert,
|
||||
beschreibt in \cite{Duong26}, wie Lean das Vertrauen in mathematische Ergebnisse
|
||||
auf eine neue Grundlage stellt.
|
||||
|
||||
\begin{description}
|
||||
\item[Algebra in Lean] Wenn Sie selbst erleben möchten, wie sich Beweisen mit
|
||||
dem Computer anfühlt, dann werfen Sie einen Blick in das Begleitskript
|
||||
\href{https://cplx.vm.uni-freiburg.de/storage/algebra-in-lean/}{„Algebra in
|
||||
Lean“}. Dort übersetzen wir ausgewählte Beweise aus diesem Skript Satz für
|
||||
Satz in Lean; über jedem Stück Code steht dabei der deutsche Originalsatz,
|
||||
sodass Sie genau verfolgen können, wie aus einem Vorlesungsbeweis ein
|
||||
formaler Beweis wird. Programmiererfahrung brauchen Sie dafür nicht. Links
|
||||
mit der Beschriftung „\textsf{Algebra in Lean}“ führen aus diesem Skript
|
||||
jeweils direkt zum passenden Kapitel des Begleitskripts.
|
||||
|
||||
\item[Natural Number Game] Beweisen mit Lean fühlt sich an wie ein
|
||||
Computerspiel und kann süchtig machen! Wenn Sie das gleich ausprobieren
|
||||
möchten: Das
|
||||
\href{https://adam.math.hhu.de/\#/g/leanprover-community/NNG4}{„Natural
|
||||
Number Game“}\index{Natural Number Game} läuft direkt im Browser, ganz ohne
|
||||
Installation. Dort bauen Sie die Arithmetik der natürlichen Zahlen aus den
|
||||
Peano-Axiomen auf -- von $2+2=4$ bis zu den Potenzgesetzen -- und lernen
|
||||
dabei spielerisch die wichtigsten Beweistechniken von Lean.
|
||||
|
||||
\item[LeanDex] Manchmal werden Sie manchmal wissen wollen, ob und unter
|
||||
welchem Namen ein bestimmter Begriff oder Satz in der Mathlib steht -- etwa
|
||||
weil Sie selbst etwas formalisieren möchten oder weil Sie neugierig sind,
|
||||
wie eine Aussage dort formuliert ist. Die Namen der Mathlib folgen strengen
|
||||
Konventionen und sind englisch; wer sie nicht kennt, braucht lange, um etwas
|
||||
zu finden. Dafür gibt es Suchmaschinen, denen Sie Ihre Frage einfach auf
|
||||
Deutsch oder Englisch stellen können:
|
||||
\href{https://leandex.projectnumina.ai}{LeanDex}\index{LeanDex} nimmt eine
|
||||
Frage in natürlicher Sprache entgegen („Wann ist eine endliche Gruppe
|
||||
zyklisch?“) und liefern die passenden Mathlib-Deklarationen samt
|
||||
Originaltext und Erklärung.
|
||||
\end{description}
|
||||
|
||||
|
||||
\subsection*{Computer-Programme}
|
||||
|
||||
Reference in new issue
Block a user