Treffer: Algebra, Logik und Beweisvisualisierung.

Im Wintersemester 2024–2025 beschäftigte sich das studentische Seminar Illustrating Mathematics an der Universität Heidelberg mit Algebra, Logik und Beweisvisualisierung. Unter Verwendung des Lean-theorem-provers (lean-lang.org) entwickelten die Studierenden dieses Seminars ein mathematisches Spiel, in dem die Spielenden aufgefordert werden, Beweise unter Verwendung der Syntax von Lean zu schreiben. Dabei wurde für das Spiel bereits existierende Infrastruktur verwendet. Der mathematische Teil wurde jedoch vollständig von den Studierenden während des Semesters produziert und implementiert. Dies bot ihnen eine neue Möglichkeit, mit Mathematik zu experimentieren und einen Einblick in das Konzept des Beweises zu gewinnen. Im Folgenden wird erläutert, wie Beweisassistenten funktionieren und wie mathematische Aussagen in Beweisassistenten formalisiert und überprüft werden können. Abschließend wird kurz die Bedeutung dieser Werkzeuge für die zukünftige mathematische Ausbildung diskutiert. [ABSTRACT FROM AUTHOR]