Computer sind immer öfter an mathematischen Durchbrüchen beteiligt. Wie Beweisprüfer und KI-Programme die Arbeit der Fachleute ändern, erklärt der Mathematiker Terence Tao im Interview.
Mathematik ist traditionell eine einsame Wissenschaft. Andrew Wiles etwa zog sich 1986 sieben Jahre in seine Studierstube zurück, um Fermats Großen Satz zu beweisen. Und die Beweise, die dabei herauskommen, sind für Kolleginnen und Kollegen häufig schwer verständlich, manche sind bis heute umstritten. Aber in den letzten Jahren sind immer größere Gebiete der Mathematik so streng in ihre einzelnen Bestandteile aufgespalten (»formalisiert«) worden, dass Beweise von Computern überprüft und verifiziert werden können.
Terence Tao von der University of California in Los Angeles ist überzeugt, dass diese Verfahren ganz neue Möglichkeiten der Kooperation in dieser Wissenschaft ermöglichen …