Proof Assistants at the interplay of mathematical cultures: a semiotic-cultural analysis of proof in higher education

In der Welt der universitären Mathematik ist der Akt des Beweisens einer Aussage mehr als nur das Lösen eines Problems; es ist eine kulturelle Praxis. Es ist eine spezifische Art des Denkens, Schreibens und Validierens von Ideen, die Studierende erlernen müssen, während sie sich von der Sekundarstufe zur Hochschulbildung bewegen. Seit Jahrzehnten beobachten Pädagogen, wie Studierende damit kämpfen, die Lücke zwischen den intuitiven, informellen Argumenten, die sie früher lernten, und den starren, expliziten Standards zu schließen, die an der Universität erforderlich sind. Kürzlich ist ein neues Werkzeug in diese Landschaft getreten: der Beweisassistent. Dies sind Computerprogramme, die darauf ausgelegt sind, mathematische Argumente mit absoluter Präzision zu prüfen, indem sie den Verfasser dazu zwingen, keinen Schritt ungeklärt zu lassen. Während einige diese Werkzeuge als Weg sehen, Mathematik rigoroser zu machen, sorgen sich andere darum, dass sie die Kreativität ersticken oder Studierende verwirren könnten, die ohnehin schon zu kämpfen haben. Die Frage ist nicht einfach, ob diese Programme helfen oder behindern, sondern wie sie das Wesen dessen verändern, wie ein Beweis geschrieben und verstanden wird.

Ein Forschungsteam zweier französischer Universitäten beschloss, diese Interaktion genau zu untersuchen. Sie fragten nicht nur, ob die Studierenden besser lernten; sie beobachteten, wie das Computerprogramm das Denkprozess der Studierenden umgestaltete. Die Studie konzentrierte sich auf einen Kurs im ersten Studienjahr, in dem die Studierenden einen spezifischen Typus eines Beweisassistenten namens Verbose Lean verwendeten. Im Gegensatz zu Standard-Programmiersprachen, die wie Code aussehen, erlaubt Verbose Lean den Studierenden, in einer kontrollierten Form der natürlichen Sprache zu schreiben, was sich eher so anfühlt, wie Mathematiker sprechen und auf Papier schreiben. Die Forscher beobachteten ein Paar Studierender bei der Arbeit an einem klassischen Problem: dem Beweis, dass wenn eine Zahlenfolge sich einem positiven Wert immer weiter annähert, die Zahlen in dieser Folge schließlich selbst positiv sein müssen. Durch die Aufzeichnung der Gespräche der Studierenden, ihrer Kritzeleien auf Papier, ihres Tippens auf dem Bildschirm und des Feedbacks des Computers erstellten die Forscher eine detaillierte Karte davon, wie eine mathematische Idee von einem groben Gedanken zu einem computerverifizierten Fakt reist.

Was die Forscher fanden, war, dass der Computer nicht nur das Endergebnis prüfte; er fungierte als Spiegel, der verborgene Annahmen offenbarte, die Studierende normalerweise als selbstverständlich voraussetzen. In einem normalen Mathematikunterricht überspringen Studierende vielleicht kleine Details oder verlassen sich auf ein „Gefühl“, dass ein Schritt offensichtlich ist. Der Computer hingegen verlangt, dass jedes einzelne Objekt, jede Bedingung und jeder logische Sprung explizit benannt und gerechtfertigt wird. Die Studie zeigte, dass diese Anforderung einen Arten von kulturellem Wandel erzwingt. Die Studierenden mussten ihre flüssigen, intuitiven Ideen in eine starre Struktur übersetzen, die die Maschine verstehen kann. Dieser Prozess verlief nicht reibungslos. Er beinhaltete ein ständiges Hin und Her zwischen den Notizen der Studierenden auf Papier, ihren gesprochenen Worten, den Fehlermeldungen des Computers und den Erklärungen des Lehrers.

Die Forscher verfolgten einen spezifischen mathematischen Ausdruck, der im Laufe der Arbeit der Studierenden immer wieder auftauchte. Zuerst behandelten die Studierenden diesen Ausdruck als eine hilfreiche Zahl, um in ihrem Argument zu rechnen. Als sie jedoch versuchten, ihn in den Computer einzugeben, lehnte das Programm ihn ab. Der Computer sagte nicht, dass die Zahl mathematisch falsch sei; er sagte, dass die Zahl am falschen Ort sei. Die Studierenden hatten versucht, sie als Bezeichnung für eine Position in einer Folge zu verwenden, aber der Computer benötigte eine ganze Zahl für diese Rolle, während ihr Ausdruck ein Bruch war. Dieser Moment war ein Wendepunkt. Er zwang die Studierenden zu der Erkenntnis, dass in der Welt des Beweisassistenten die Rolle, die eine Zahl spielt, genauso wichtig ist wie die Zahl selbst. Sie mussten ihre Strategie überdenken und den Ausdruck in einen anderen Teil ihres Arguments verschieben, wo er schließlich in die strengen Regeln des Computers passte.

Dieser Kampf wurde nicht allein durch den Computer gelöst. Der Lehrer, der im selben Klassenzimmer an der Tafel arbeitete, zeichnete ein Diagramm, um das Konzept visuell zu erklären. Er beschrieb ein „Fenster“ der Größe, das den Studierenden half zu sehen, warum ihre Zahl kleiner als der Zielwert sein musste. Diese visuelle Erklärung, kombiert mit der Ablehnung ihres ersten Versuchs durch den Computer, half den Studierenden, ihre Gedanken zu reorganisieren. Sie erkannten schließlich, dass die Zahl, mit der sie gekämpft hatten, nicht die Position in der Folge war, sondern die Größe der Lücke, die sie messen mussten. Sobald sie diesen Wechsel vollzogen hatten, akzeptierte der Computer ihr Argument. Der endgültige Beweis war keine gerade Linie von der Idee zur Lösung; es war eine komplexe Reise, auf der sich die Bedeutung eines einzelnen Symbols änderte, je nachdem, ob es gesprochen, auf Papier geschrieben, von einem Lehrer erklärt oder von einer Maschine geprüft wurde.

Die Studie legt nahe, dass Beweisassistenten als „epistemische Enthüller“ fungieren, ein Begriff, den die Autoren verwenden, um Werkzeuge zu beschreiben, die das Unsichtbare sichtbar machen. Sie enthüllen die „Un-Gedanken“ der Mathematik – jene Teile eines Beweises, die Experten und Studierende normalerweise ungesagt lassen, weil sie offensichtlich erscheinen. In einem traditionellen Klassenzimmer könnten diese Lücken unbemerkt bleiben. In einem Klassenzimmer mit einem Beweisassistenten zwingt der Computer den Studierenden dazu, jede Lücke zu füllen und die verborgenen Regeln offenzulegen, die die mathematische Gültigkeit bestimmen. Die Forscher argumentieren, dass dies nicht bedeutet, dass der Computer besser als der Mensch ist oder der Mensch besser als der Computer. Stattdessen arbeiten die beiden Systeme zusammen, um einen neuen Raum zu schaffen, in dem verschiedene Arten, über einen Beweis zu denken, kollidieren und verschmelzen.

Die Ergebnisse deuten darauf hin, dass die Einführung dieser Werkzeuge die Kultur des Beweisens in der Hochschulbildung verändert. Es geht nicht nur darum, eine Ebene technischer Rigorosität hinzuzufügen; es geht darum, das Verständnis darüber, was es bedeutet, „richtig“ zu sein, neu zu konfigurieren. Die Studie zeigt, dass Studierende nicht einfach lernen, Code zu schreiben; sie lernen, zwischen verschiedenen Welten der Bedeutung zu navigieren. Sie müssen lernen, ihr intuitives Verständnis in eine Sprache zu übersetzen, die eine Maschine verifizieren kann, während sie gleichzeitig auf die menschliche Erklärung des Lehrers hören. Die Fehlermeldungen des Computers sind nicht bloß Hindernisse; sie sind Signale, die den Studierenden mitteilen, wo ihr Verständnis unvollständig ist. Indem sie die Studierenden dazu zwingen, ihre impliziten Annahmen explizit zu machen, bieten diese Werkzeuge eine einzigartige Gelegenheit, zu untersuchen, wie mathematisches Wissen aufgebaut und validiert wird.

Letztlich kommt das Paper zu dem Schluss, dass Beweisassistenten keine neutralen Werkzeuge sind. Sie tragen spezifische Vorstellungen darüber in sich, was als ein gültiges Argument zählt. Wenn Studierende sie verwenden, lernen sie nicht nur Mathematik; sie lernen einen neuen Satz kultureller Regeln dafür, wie man denkt und kommuniziert. Die Forscher legen nahe, dass dieser Wandel einen privilegierten Ort bietet, um die Kontinuitäten und Brüche zwischen der Art und Weise, wie Beweise gelehrt werden, der Art und Weise, wie sie von Experten praktiziert werden, und der Art und Weise, wie sie von Maschinen geprüft werden, zu untersuchen. Die Reise der Studierenden in dieser Studie, von ihrer anfänglichen Verwirrung bis zu ihrem endgültigen Erfolg, illustriert, dass das Lernen des Beweisens mit einem Computer ein Prozess der Übersetzung ist. Es ist ein Prozess, in dem die Bedeutung einer mathematischen Idee getestet, umgestaltet und letztlich durch die Interaktion von menschlicher Intuition, menschlicher Anleitung und maschineller Präzision stabilisiert wird.