Um abstrakte mathematischen Aussagen per Computer prüfen zu lassen, gibt es inzwischen einen etablierten Formalismus, der auf der Computersprache LEAN basiert. Prof. Zibrowius: „In absehbarer Zeit wird kein Mathematiker mehr um diese formalisierte, computerverarbeitbare Beweisführung herumkommen. Es ist deshalb wichtig, dass wir unsere Studierende an diese Zukunftstechnologie heranführen.“
Prof. Zibrowius und einige Mitarbeiter haben dazu die Open Educational Ressources-Plattform „Lean Game Server“ ins Leben gerufen, eine graphische Nutzeroberfläche für die Programmiersprache LEAN implementiert und das Lernspiel „Robo“ entworfen, das durch verschiedene mathematische Beweisverfahren führt. Mit Hilfe von Robo können die Spielenden Schritt für Schritt prüfen, ob ihre Beweisführung richtig ist oder ob es darin logische Fehler gibt.
Ben Steinhauer ist einer der Studierenden, die die Plattform bereits ausprobiert haben: „Der spielerische Zugang erleichtert es sehr, sich in den Formalismus einzuarbeiten. Beginnend mit dem Beweis, dass 42=42 ist, über induktive Beweise, arbeiten sich die Spieler Schritt für Schritt zu komplizierteren Beweismethoden vor. Sie erhalten jeweils gleich Rückmeldungen, ob sie auf dem richtigen Weg sind.“
Zibrowius: „Wir haben das System bereits in mehreren Bachelor-Seminaren eingesetzt, es wird sehr gut von den HHU-Studierenden angenommen. Und es wird Monat für Monat von hunderten Studierenden weltweit genutzt.“
Nach einer bereits abgeschlossenen dreijährigen Aufbauphase, die die Stiftung Innovation in der Hochschullehre unterstützt hat, fördert nun die Stiftung Renaissance Philanthropy die kontinuierliche Weiterentwicklung des öffentlich zugänglichen Systems im Rahmen eines „AI for Math Fund“. Der Server wird vom Zentrum für Informations- und Medientechnologie der HHU bereitgestellt.
Zum HHU-Spielserver
