Könnten Computer und Programme wie der Beweisprüfer Lean die Mathematik retten? Diese Frage stellen sich Forschende weltweit angesichts einer immer komplexer werdenden Disziplin. Denn die Mathematik steht heute vor einem grundlegenden Problem: Sie ist so stark spezialisiert und kompliziert geworden, dass oft nur noch wenige Expertinnen und Experten weltweit in der Lage sind, bestimmte Beweise vollständig nachzuvollziehen. Das erschwert die unabhängige Überprüfung und erhöht die Gefahr, dass Fehler unentdeckt bleiben.
Lean — die Lösung?
Gleichzeitig wächst die Zahl neuer Arbeiten rasant, sodass niemand mehr den Überblick behalten kann. Genau hier setzen Computer mit Programmen wie Lean an. Diese sogenannten Beweisprüfer helfen, die Mathematik in eine formale Sprache zu übersetzen, die Maschinen dann Schritt für Schritt überprüfen können. Die Hoffnung ist neben der Vermeidung von Fehlern auch, dass die Ergebnisse so wieder für alle Fachleute nachvollziehbar werden.
Seit den 2010er Jahren wächst die „Formalisierungs-Community“, die neben Lean auch mit Projekten wie „Mathlib“ bereits Millionen Zeilen mathematischer Definitionen und Sätze in Code überführt hat.
Zudem ermöglichen digitale Plattformen eine neue Form der Zusammenarbeit: Forschende, Studierende und Interessierte weltweit können gleichzeitig an Teilaufgaben arbeiten und so gemeinsam selbst komplizierteste Beweise prüfen. Ein aktuelles Beispiel: Eine Gruppe von deutschen Schülerinnen und Schülern beschäftigte sich intensiv mit dem berühmten Banach-Tarski-Paradoxon und entschlüsselte es mit einem Computer.
Programme wie Lean und die Kraft der künstlichen Intelligenz sollen solche Prozesse in Zukunft noch beschleunigen. Damit könnte die Mathematik nicht nur zuverlässiger, sondern auch kollaborativer und zugänglicher werden — und sich von einem einsamen Expertenspiel zurück in einen echten Teamsport verwandeln.
Die Mathematik als Disziplin ist super fragmentiert.
Manon Bischoff
Manon Bischoff ist Redakteurin für Mathe und Physik bei Spektrum der Wissenschaft. Im Gespräch mit detektor.fm-Moderator Marc Zimmer erklärt sie, worin eines der größten Probleme der modernen Mathematik besteht und wie Computer und KI in Zukunft helfen sollen, es zu lösen.