antaris
Registriertes Mitglied
Ich will hier im Thread Schritt für Schritt die lean-Konstruktion durchgehen.
Das Ziel ist nicht das präsentieren des ganzen codes, sondern tatsächlich das Verstehen der Konstruktion in lean.
Ich will selber verstehen, was da "passiert" und darum ist es m.E sinnvoll genauso "from scratch" anzufangen, wie der code selber.
Wobei "from scratch" nicht allzu überbewertet werden sollte, da ja schließlich nicht mit Nichts angefangen wird.
Darum sollte nicht direkt mit Wörter, Monoide oder gar Bäume angefangen werden. Die Voraussetzungen liegen in lean selbst, auch wenn diese durch Verbot von mathlib, sowie der lean-eigenen Zahlentheorie stark begrenzt sind. Aber die lean-Grundlagen sollten zuerst verstanden werden, bevor man die Formalisierung damit versucht zu verstehen.
Der Vorteil ist, dass tatsächlich alle Operationen "offen verdrahtet" sind und fast nichts hinter großen Libraries "verschwindet". Man kann also wirklich fast alle Anschlüsse und Verbindungen direkt im code nachvollziehen.
Code-Basis ist der bereits geteilte Stand:
Wobei ich das PDF nicht unbedingt als die primäre Quelle behandeln wollen würde, sondern direkt den code. Das Repo liegt vollständig und entpackt auf github und so ist es einfach direkt die Module zu verlinken. Je nachdem wie das hier läuft, könnten die entsprechenden Stellen im PDF zusätzlich referenziert werden.
Ansonsten natürlich auch die Frage, ob das hier überhaupt jemand unterstützen will bzw. ob es interessiert. Ich würde es toll finden aber wenn nicht, dann ist es auch ok. Wenn aber doch, dann bitte ich um eine konstruktive Diskussion. Es geht zuerst nur im die wohl eher langweiligen aber dafür grundlegenden Konstruktionen, noch keine Implikationen/Interpretationen/Konstruktionen in Richtung DtN/Laplacian/Vervollständigungen/effektive Geometrien/Widerstände usw.
Genau genommen ist der Titel des PDF's schon nicht ganz korrekt, da in lean nicht zuerst mit Wörter angefangen wird.
Ich vermute, dass das Thema bis Q allein schon anspruchsvoll genug ist, wenn man wirklich alle Schritte durchgehen will. Das ist m.E. nicht in ein paar Tage erledigt. Wenn das durch ist, dann könnte auf den erweiterten code übergegangen werden, der dann aus physikalischer Sicht sehr wahrscheinlich viel interessanter ist, wenn das ganze nicht sogar schon vorher zerbricht.
Ich habe selber noch keinen wirklich vollständigen Plan, wie man wirklich anfangen sollte aber ich denke es ist nötig einen gewissen Standard zu etablieren, wie ein Lernthema überhaupt dargestellt werden sollte.
Ich dachte mir etwas sowas in der Art:
Vorlage für eine Lerneinheit
1. Fragestellung: Welches einzelne mathematische Problem wollen wir verstehen?
2. Voraussetzungen: Welche Begriffe und Lean-Mechanismen dürfen wir bereits verwenden?
3. Originaldefinition: Exakter Ausschnitt aus der betreffenden Quelldatei, möglichst mit Commit-Link und Zeilenangabe.
4. Mathematische Übersetzung: Was bedeutet die Definition unabhängig von der Lean-Syntax?
5. Beweis: Welche Aussage folgt daraus, und welche Beweisschritte verwendet Lean tatsächlich?
6. Kritische Prüfung: Welche Voraussetzungen wurden übernommen, was wurde nicht bewiesen und welche stärkere Behauptung wäre unzulässig?
7. Verständniskontrolle: Ein kleines Beispiel oder Gegenbeispiel, das den Unterschied zwischen Definition und Theorem sichtbar macht.
Man könnte die Hauptthemen in Abschnitte A-G unterteilen.
- Abschnitt A – Die logischen Voraussetzungen von Lean
- Abschnitt B – Induktive Pfade und natürliche Zahlen
- Abschnitt C – Vom Pfad zum endlichen Wortbaum
- Abschnitt D – Konstruktion der ganzen Zahlen
- Abschnitt E – Von Ganzzahlen zu rationalen Bruchdaten
- Abschnitt F – Die eigentliche rationale Pfadkonstruktion
- Abschnitt G – Ordnung, Einbettungen und Unabhängigkeit der Verzweigung
und diese Hauptthemen wiederum in Unterthemen unterteilen:
| Nr. | Thema | Was verstanden werden muss |
|---|---|---|
| 01 | Formale Mathematik und Lean | Unterschied zwischen mathematischer Aussage, Definition, Theorem, Beweisterm, Elaborator und Kernel. Was heißt maschinell geprüft? |
| 02 | Typen und Universen | Sort, Prop, Type, Type u, Elemente, Typzugehörigkeit und Universe-Polymorphie. |
| 03 | Funktionen und abhängige Typen | Funktionen als Terme, Lambda-Abstraktion, Anwendung, ∀, Π, implizite Argumente und Abhängigkeit von Werten. |
| 04 | Aussagen und Logik | Curry-Howard-Korrespondenz, True, False, And, Or, Exists, Negation, konstruktive Existenzbeweise. |
| 05 | Induktive Typen | Konstruktoren, Rekursionsprinzip, Induktionsprinzip, Mustervergleich und Terminierung. |
| 06 | Gleichheit und Beweise | Definitorische vs. propositionale Gleichheit, rfl, Eq.rec, rw, congrArg, funext und Beweisirrelevanz. |
| 07 | Strukturen und Typklassen | structure, abhängige Felder, beweistragende Daten, class, instance, Decidable und DecidableEq. |
| 08 | Quotienten und Axiome | Äquivalenzrelationen, Quot.mk, Quot.sound, Quot.lift, Quot.ind, Verträglichkeitsbeweise, propext, Axiom-Audits. |
Bis Abschnitt G wären es insgesamt 33 Unterthemen.
Das zeigt: man braucht hier Geduld...
Also was sagt ihr dazu?
Zuletzt bearbeitet: