Spielend Beweisen lernen mit Lean4

12. Oktober 2026 Leonid Ryvkin Lesezeit: 3 Minuten Auf Mastodon ansehen

In diesem Artikel geht es um die Programmiersprache Lean, die es erlaubt, mathematische Beweise zu führen, und ein Spiel, welches dabei helfen kann, Lean zu lernen.

Was ist ein mathematischer Beweis

Eine der grössten Schwierigkeiten für viele Studierende mathematisch-naturwissenschaftlicher Fächer im ersten Semester ist das Konzept des Beweisens. Am Anfang der Schulzeit rechnet man mit Zahlen, später mit Variablen, man wendet Rechenregeln oder Formeln an, aber vielerorts lernt man nie wirklich, warum diese Formeln überhaupt gelten.

Ein Beispiel für eine Formel wäre so etwas wie x < 2 * x ('das Doppelte einer Zahl ist grösser als die Zahl selbst') und ein Beweis der Formel wäre ein stichhaltiges Argument, warum diese Formel immer gilt (ein solcher Beweis kann natürlich nur für x existieren, welches grösser als Null ist, denn 2 * (-1) = -2 ist kleiner als -1). Eine der Schwierigkeiten beim Beweisen lernen ist mangelndes Feedback: Wenn man rechnet und zu einem falschen Ergebnis kommt, weiss man, dass man sich verrechnet hat. Wenn man für eine richtige Formel einen Beweis angibt, kann es sehr kompliziert sein, herauszufinden, ob der Beweis korrekt ist, und, wenn nicht, einen Fehler zu finden. In der mathematischen Forschung, die sich zu grossen Teilen mit Beweisen beschäftigt, dauert es manchmal Jahre, bevor ein Beweis als korrekt anerkannt wird (oder widerlegt wird). Ein Extrembeispiel hierfür ist diese Kontroverse. Ein Beweis enthält häufig eine Kette von Umformungen und Argumenten, und es kann sehr schwierig sein, zu erkennen, an welchem Kettenglied man etwas übersehen hat. Abhilfe dazu schaffen Beweisassistenten, wie Lean4.

Was sind Beweisassistenten

Ein Beweisassistent besteht aus einer Programmiersprache, die es erlaubt, mathematische Aussagen und Beweise zu formulieren, und einem Programm, welches prüft, ob die gegebenen Argumente stimmen. Lean4 ist ein sehr populärer Beweisassistent und unter der Apache-2.0-Lizenz veröffentlicht. Die offizielle Installationsanleitung schlägt Installation über ein Plugin für VS Code vor, aber die Open-Source-Version Code - OSS funktioniert auch. Es gibt auch eine Live-Version online, für die man nichts installieren muss.

Ein Beispielbeweis in Lean4

Ein Beispiel für einen Beweis der oben gegebenen Formel wäre:

import Mathlib
theorem meineFormel (x : ℝ) (meineBedingung : 0 < x) : x < 2 * x := by
  rw [two_mul]
  apply lt_add_of_pos_right
  exact meineBedingung

Die erste Zeile lädt die mathematische Bibliothek Mathlib von Lean. Die zweite Zeile formuliert den Satz, den wir beweisen wollen: Der Satz heisst meineFormel und hat als Eingabeinformation eine (reelle) Zahl x und die Bedingung meineBedingung die besagt, dass diese Zahl grösser als Null ist. Daraufhin folgt die Aussage des Satzes, die Formel x < 2 * x. Der Ausdruck := by leitet den Beweis ein. Die nächsten zwei Zeilen beschreiben die Umformungen, die nötig sind, um die zu beweisende Aussage x < 2 * x auf die bereits bekannte 0 < x zurückzuführen. Die letzte Zeile besagt 'Das, was jetzt noch zum Beweis fehlt, ist genau die Bedingung meineBedingung, die ja bereits gegeben ist.'

Wenn man das Programm in der Live-Version (oder auf dem eigenen Computer) laufen lässt, sieht es ungefähr wie folgt aus:

Auf der linken Seite befindet sich das Editor-Fenster und auf der rechten die Lean4-Informationsansicht. Letztere beschreibt den aktuellen Zustand des Beweises, an der Stelle, an der sich gerade der Cursor befindet. Das Symbol ⊢ ist dabei die Schreibweise für 'Das musst du noch beweisen'. Im Screenshot befindet sich der Cursor am Anfang der Zeile 4, das heisst, der Befehl rw [two_mul] wurde bereits angewendet und der Ausdruck 2*x in der ursprünglich zu beweisenden Aussage wurde bereits durch x + x ersetzt. Dementsprechend muss nur noch x < x + x bewiesen werden.

Spielend Beweisen lernen

Um herauszufinden, was rw, apply und so weiter bedeuten, kann man die Lean4-Dokumentation lesen, aber diese ist sehr technisch und eher hilfreich, wenn man bereits Expertin ist. Eine andere Möglichkeit sind Lean-Lern-Spiele. Dies sind kleine Online-Spiele, mit denen man Schritt für Schritt lernt, Beweise zu führen und in Lean zu formulieren. Zwei der Spiele (Zahlenspiele und Robo) haben bereits deutsche Übersetzungen, ich würde für den Anfang Zahlenspiele empfehlen, auch wenn das schöne Titelbild des Artikels aus dem Spiel Robo kommt.

Titelbild: https://adam.math.hhu.de/#/g/hhu-adam/robo/world/Logo/level/0

Quellen:

https://de.wikipedia.org/wiki/Lean_(Beweisassistent)

https://adam.math.hhu.de/#/