D2 | Du beweist noch händisch?!
A) Ein Einblick in maschinengestützte mathematische Beweise
Was genau ist ein mathematischer Beweis? Und sind Computer in der Lage, originelle Beweise zu finden? Beweise stehen im Zentrum der Mathematik: Ein charakteristisches Merkmal dieses Fachgebiets besteht darin, Hypothesen durch sorgfältige Argumentation zu überprüfen, auch mit Hilfe von Computern. Potentiell eröffnen dabei Fortschritte im Bereich maschinellen Lernens und insbesondere der Large Language Models neue Möglichkeiten, Mathematiker*innen zu helfen. Wie lange wird Mathematik noch ohne Unterstützung von künstlicher Intelligenz gemacht?
B) Bedeutung und Geschichte der Beweise in der Mathematik
Welche Funktion erfüllen Beweise in der Mathematik? Um besser zu verstehen, was überhaupt ein mathematischer Beweis ist, welche Rolle er spielt und wann er gültig ist, befragen wir die Mathematikgeschichte: von Euklid über Weierstrass, Russell und Gödel hin zu computergestützten und »formalen« Beweisen mit Hilfe von Computern. Dabei wollen wir beispielhaft einige Beweistechniken konkret kennenlernen und an Beispielen anwenden (insbesondere für Teilnehmende aus anderen Fachrichtungen, die keine Grundvorlesungen in Mathematik besucht haben). Außerdem wollen wir lückenhafte, mangelhafte und fehlerhafte Beweise und den Umgang damit in der Mathematikcommunity diskutieren.
C) Formale gegenüber informellen Beweisen
Wie lassen sich Beweise »absichern« und formalisieren? Können Menschen hinreichend abgesicherte und formalisierte Beweise noch verstehen und erklären? Wir wollen verstehen, was computergestützte Beweise sind, und was formale Beweise sind. Dafür schauen wir uns einige bekannte Beweise an, die nur mit Computerhilfe möglich waren. Ein praktischer Teil des
Seminars bietet die Gelegenheit, mit Hilfe des interaktiven Beweisprüfers »Lean« direkte Erfahrungen im Umgang mit formalen Beweisen zu sammeln.
D) Wie können Computer Mathematiker*innen assistieren?
In den letzten zehn Jahren gab es große Fortschritte im Bereich maschinellen Lernens, die zum Beispiel dazu geführt haben, dass Computer inzwischen besser Go spielen als Menschen. Das Reinforcement Learning, welches diese Erfolge ermöglichte, wurde auch erfolgreich in einer Reihe von anderen Problemen angewendet, zum Beispiel bei der Proteinfaltung, aber auch in
mathematischen Anwendungen.
Large Language Models sind mittlerweile in der Lage, verschiedene Dinge zu tun: z. B.
· Mathematikaufgaben aus dem Schulunterricht (und allen anderen Fächern) zu lösen,
· zwischen verschiedenen Sprachen zu übersetzen,
· simple Computerprogramme zu schreiben.
Bei welchen Aufgaben in der Mathematik können solche Methoden aus dem Bereich des maschinellen Lernens hilfreich sein? Einiges dabei wird spekulativ sein und wir wollen auch diskutieren, ob es prinzipielle Grenzen bei der Anwendung solcher Methoden gibt. Ebenso soll die Frage erörtert werden, inwieweit sich die Situation in der Mathematik auf andere Wissenschaften
übertragen lässt.
Seminarleitung: Moritz Firsching, Nikolas Kuhn
Die Anmeldung erfolgt über das Intranet.