diff --git a/.gitignore b/.gitignore index ad39524..0892ac9 100644 --- a/.gitignore +++ b/.gitignore @@ -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 diff --git a/.vscode/ltex.dictionary.de-DE.txt b/.vscode/ltex.dictionary.de-DE.txt index 0745869..8fe5521 100644 --- a/.vscode/ltex.dictionary.de-DE.txt +++ b/.vscode/ltex.dictionary.de-DE.txt @@ -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 diff --git a/00.tex b/00.tex index a713bf8..3873242 100644 --- a/00.tex +++ b/00.tex @@ -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}