Talkrunde: Formalisierung der Mathematik - Wann führen Computer die Beweise?

Im Rahmen der 5. Bonner Mathenacht am 29.04.2022,, organisiert vom Hausdorff Center for Mathematics, fand eine Talkrunde zum Thema "Formalisierung der Mathematik - Wann führen Computer die Beweise?" statt. Teilnehmer*innen waren:

Prof. Dr. Erika Abraham (RWTH Aachen),
Prof. Dr. Peter Koepke (Mathematisches Institut, Universität Bonn),
Prof. Dr. Michael Kohlhase (Universität Erlangen-Nürnberg),
Prof. Dr. Peter Scholze (Max-Planck-Institut für Mathematik und Mathematisches Institut, Universität Bonn).

Moderiert wurde die Talkrunde von Dr. Thoralf Räsch, die Mathenacht selbst von Stefan Hartmann.

Zum Inhalt der Talkrunde:
Mathematiker*innen beweisen ihre Theoreme in der Regel zwar exakt, aber nicht im strengen Sinne formal. Kleinere Beweissprünge oder intuitiv vorgetragene Argumente in längeren Beweisen sind üblich. Ob ein Beweis korrekt ist und ob ein mathematischer Satz als bewiesen gilt, entscheidet die Forschungsgemeinschaft heutzutage durch Peer-Review-Verfahren, also letztendlich durch einen Konsens. Hierbei besteht prinzipiell die Möglichkeit von Fehleinschätzungen. Informelle Beweise lassen sich jedoch in formale Beweise umformen. Ein formaler Beweise beginnt mit Axiomen und leitet aus diesen die Behauptung ab, wobei jeder Schritt der Beweisführung die Anwendung einer genau definierten logischen Regel ist. Solche Beweise können von Computern auf Korrektheit überprüft werden. Außerdem können Computer selbst formale Beweise erzeugen und damit möglicherweise auch interessante Resultate automatisch beweisen. Utopisch erscheint es längst nicht mehr, dass dies zum Standard wird. Gerade in jüngster Zeit hat sich das Feld sehr dynamisch entwickelt; wir stehen kurz vor einer Schwelle in ein neues Zeitalter der mathematischen Beweisführung. Selbst hochkomplexe Aussagen lassen sich mittlerweile formalisieren, wie am "Liquid Tensor Experiment" gezeigt wurde. Diese hatte Peter Scholze seinen Kolleg*innen als Herausforderung gestellt und über das Ergebnis in der Talkrunde berichtet. Was sind die Konsequenzen dieser Entwicklung? Akzeptiert die mathematische Community tatsächlich einen solchen Paradigmenwechsel? Welche Rolle nehmen dann noch Mathematiker*innen ein? In der Talkrunde haben wir uns mit solchen Fragestellungen beschäftigt, den Stand der Forschung präsentiert und über weitere Entwicklungen diskutiert.