- Lean ist eine Programmiersprache, die für die Formalisierung von Mathematik entwickelt wurde und es Mathematiker:innen ermöglicht, mathematische Sätze wie Code zu behandeln.
- Nutzer schreiben Satz, Beweis, Axiom etc. in Codeform; der Beweisablauf wird über ein Befehlsset namens tactic durchgeführt.
- Ein Beweis muss nicht vollständig fertiggestellt sein, er kann aber mit
sorry vorläufig abgeschlossen werden; das ist jedoch ein falscher Beweis ähnlich any in TypeScript.
- Wird ein falsches Axiom hinzugefügt (z. B.
2 = 3), entsteht das Risiko eines logischen Widerspruchs und der Beweisbarkeit jeder Behauptung.
- Lean leitet Schlussfolgerungen nur aus den logisch ausgewählten Axiomen und dem Beweissystem ab, daher hat die Aufrechterhaltung mathematischer Gültigkeit große Bedeutung.
Lean: Mathematik als Code behandeln
- Lean ist eine Programmiersprache, die auf formalisiertes Mathematikschreiben spezialisiert ist.
- Mit Lean können Mathematiker mathematische Sätze und Beweise in Codeform ausdrücken und so strukturieren, dass sie kooperativ geteilt werden können.
- Es entwirft eine mögliche Zukunft, in der ein Großteil des mathematischen Wissens in Codeform vorliegt und mechanisch verifiziert sowie kombinierbar wird.
Der erste Schritt eines Lean-Beweises
- In Lean ist eine einfache Theorem-Deklaration der Form
theorem two_eq_two : 2 = 2 := by sorry möglich.
- Wenn ein Beweis unvollständig ist, kann
sorry verwendet werden, aber das ist nur ein vorläufiger Schritt, kein echter Beweis.
sorry lässt die Beweisprüfung von Lean passieren, ist jedoch logisch nicht vertrauenswürdig.
- Für vollständige Beweise wird eine Taktik wie
rfl (Reflexivität) verwendet, um offensichtliche Gleichungen wie 2 = 2 zu beweisen.
- Bereits bewiesene Inhalte können mit
exact usw. in anderen Theoremen wiederverwendet werden, was die Modularität betont.
Axiome und Widerspruch: Wenn die Mathematik von einem Gespenst heimgesucht wird
- Wenn ein Axiom wie
axiom math_is_haunted : 2 = 3 hinzugefügt wird, betrachtet Lean dies als wahr.
- Dieses Axiom kann anschließend im Beweisprozess verwendet werden und sogar mathematisch unsinnige Schlussfolgerungen (z. B.
2 + 2 = 6) werden beweisbar.
- Es ist möglich, mit der Tactic
rewrite 2 durch 3 zu ersetzen und den Beweis mit rfl abzuschließen.
- Wenn ein ungeeignetes Axiom zu einem Widerspruch führt, kann in Lean der Zustand eintreten, dass jede Aussage beweisbar ist (logischer Kollaps).
- Tatsächlich führte etwa Russells Paradoxon zu Beginn des 20. Jahrhunderts dazu, dass Inkonsistenzen in Axiomensystemen zu einer grundlegenden Fragestellung der Mathematik wurden.
- So zeigt Lean eindrücklich, dass die Wahl der Axiome entscheidend für die Aufrechterhaltung der logischen Konsistenz eines Systems ist.
Lean als Beweisprüfer
- Sind die Axiome gut gewählt und Lean ist logisch korrekt, liefert es theoretisch verlässliche Schlüsse.
- Von einfachen Gleichungen bis zu sehr komplexen Sätzen (z. B. Fermat's Last Theorem) werden alle nach denselben Prinzipien geprüft.
- Bei großen Theoremen entsteht der vollständige Beweisbaum durch wiederholtes, aufeinander aufbauendes Beweisen von Unterstrukturen und Sätzen.
- Als Beispiel wird ein großes Projekt beschrieben, das Fermat's Last Theorem in Lean formalisiert, mit dem Ziel, dass am Ende ein vollständiges Beweissystem ohne
sorry steht.
Die Freude am Lernen von Lean
- Das Beweisen in Lean ist eine kreative Verbindung von Programmierung und Mathematik.
- Anfangs geht es darum, einfache Aussagen zu beweisen; allmählich wird der Prozess, schrittweise immer komplexere und tiefere Mathematik rigoros aufzubauen, zur eigentlichen Freude.
- Offizielle Tutorials und Community-Materialien (z. B. Natural Numbers Game, Mathematics in Lean usw.) eignen sich gut für den Einstieg.
- Mit Lean formalisierst du die Logik direkt selbst und entdeckst die Schönheit hinter raffinierten Ideen und Argumenten erneut.
- Das Fazit lautet: Für manche Menschen macht Lean einfach besonderen Spaß, auch ohne äußeren Anlass.
Noch keine Kommentare.