Tech

Dieser Zahlentheoretiker befürchtet, dass viele unserer Mathe-Grundlagen falsch sind

GettyImages-908884386

Es sei Zeit, eine neue Ära der Mathematik einzuleiten, findet Kevin Buzzard. Der britische Zahlentheoretiker und Mathematikdozent am Imperial College London will, dass Computer eine größere Rolle in der reinen Mathematik spielen, insbesondere bei Beweisen. Mathematische Beweise sind so komplex geworden, dass kein Mensch sie in all ihren Einzelheiten verstehen kann, geschweige denn sie verifizieren. Buzzard befürchtet, dass viele anerkannte Beweise in Wahrheit falsch sind.

Was ist ein mathematischer Beweis? Mit einem Beweis demonstriert man, dass eine mathematische Annahme richtig ist. Mit jedem Beweis wächst unser Wissen über die Mathematik – und dieses sickert dann in andere Bereiche ein.

Videos by VICE

Für einen Beweis braucht man zunächst ein paar Definitionen. Zum Beispiel definiert man eine Zahlenmenge wie alle ganzen Zahlen, also jede Zahl von minus unendlich bis plus unendlich. Als Nächstes formuliert man ein Theorem. Zum Beispiel: Es gibt keine größte ganze Zahl. Der Beweis selbst ist dann die logische Argumentation, die darlegt, ob das Theorem richtig oder falsch ist – in diesem Fall richtig. Die logische Herleitung in dem Beweis beruht auf anderen, bereits bewiesenen mathematischen Wahrheiten – zum Beispiel, dass 1 kleiner als 2 ist.



Auch bei VICE: Die Mathematik eines Massenaufstands


Weil die Menschheit schon seit Tausenden Jahren Mathematik betreibt, bauen moderne Beweise auf einer Vielzahl vorangegangener Erkenntnisse auf. Buzzard sagt allerdings, dass in vielen Fällen die alten Beweise, auf denen die neuen Beweise fußen, nicht eindeutig verstanden worden seien. Es gebe wichtige wissenschaftliche Arbeiten, die sich offen auf unveröffentlichte Werke beziehen. Das bereitet Buzzard Sorgen.

“Ich befürchte, dass die ganze veröffentlichte Mathematik falsch ist, weil Mathematiker die Einzelheiten nicht kontrollieren – und ich schon mal gesehen habe, dass sie falsch liegen”, sagt Buzzard zu VICE.

“Die Wahrscheinlichkeit, dass einige unserer großen Schlösser nicht auf Sand gebaut sind, geht meiner Meinung nach gegen Null”, schrieb Buzzard in einer Präsentation.

Eigentlich sollten neue mathematische Theoreme von Grund auf bewiesen sein. Jeder Schritt muss kontrolliert werden. Andererseits spielen in der Mathematik erfahrene und angesehene Expertinnen und Experten eine wichtige Rolle. Wenn einer dieser Weisen einen Aufsatz zitiert und sich in seiner Arbeit darauf beruft, muss dieser Aufsatz wahrscheinlich nicht noch mal kontrolliert werden – so jedenfalls die weit verbreitete Einstellung.

Buzzard wirft der modernen Mathematik vor, zu sehr von diesem erlesenen Kreis der Weisen abhängig zu sein. Ein neuer Beweis zitiert vielleicht 20 andere Arbeiten und nur eine einzelne davon kann 1.000 Seiten dichter und komplexer Beweisführung umfassen. Wenn dann eine respektierte Mathematikerin die 1.000-Seiten-Arbeit in einem eigenen Beweis zitiert, gehen viele andere Mathematiker davon aus, dass die zitierte Arbeit und der neue Beweis richtig sind. In der Regel macht sich dann keiner die Mühe, alles noch einmal zu kontrollieren.

Den 1994 veröffentlichen Beweis für eins der schwierigsten mathematischen Probleme überhaupt, den Großen Fermatschen Satz aus dem 17. Jahrhundert, hat laut Buzzard niemand wirklich verstanden.

“Ich glaube, dass kein Mensch, tot oder lebendig, alle Details dieses Beweises kennt. Aber die mathematische Gemeinschaft hat den Beweis des Großen Fermatsches Satzes trotzdem akzeptiert”, schrieb Buzzard in einer Präsentation. “Weil die Weisen entschieden haben, dass der Beweis OK ist.”

Vor ein paar Jahren hörte Buzzard in Vorträgen der Mathematikgrößen Thomas Hales und Vladimir Voevodsky zum ersten Mal von Software für die Beweisprüfung. Mit dieser lassen sich Beweise systematisch von einem Computer bestätigen.

Als Buzzard selbst mit einem solchen Programm, Lean, zu arbeiten begann, war er sofort gefesselt. Nicht nur erlaubte ihm die Software, Beweise über alle Zweifel erhaben zu prüfen, sie förderte auch mathematisches Denken in klarer und unmissverständlicher Weise.

“Computer akzeptieren nur sehr präzise Eingaben, was auch meiner präferierten Herangehensweise an die Mathematik entspricht”, sagt Buzzard. “Ich verliebte mich, weil ich das Gefühl hatte, einen Seelenpartner gefunden zu haben. Dieses Programm dachte über Mathematik wie ich.”

Um einen Beweis mit Lean zu verifizieren, muss man den Beweis formalisieren oder von menschlicher Sprache und Symbolen in die Programmiersprache von Lean umwandeln. Das gilt auch für auch alle untergeordneten Beweise und Definitionen, auf denen die neue Arbeit beruht. Auch wenn dieser Prozess sehr arbeitsintensiv ist, scheint Lean mit allen mathematischen Aufgaben klarzukommen, mit denen Buzzard es füttert – das unterscheidet Lean von anderer vergleichbarer Software.

Auch deswegen hat Lean das Interesse von immer mehr Mathematikern geweckt, insbesondere in der Lehre. Jeremy Avigad ist Dozent mit dem Schwerpunkt Beweistheorie an der Carnegie Mellon University in Pittsburgh. Er und Buzzard haben begonnen, Lean in Einführungsseminaren der Beweistheorie einzusetzen. Die Software prüft jeder Zeile eines Beweises und gibt Feedback, was für Studierende besonders hilfreich ist.

Obwohl Avigad vom zunehmenden Interesse an Lean begeistert ist, mahnt er zur Vorsicht. Die Software benötige noch Verbesserungen. Der Einsatz solcher Beweisassistenten sei vor allem zeitintensiv. “Den Bereich gibt es seit ein paar Jahrzehnten und es wird immer besser, aber wir sind noch nicht so recht am Ziel angekommen”, sagt er.

Wenn diese Hürden überwunden werden, könnte die Software laut Buzzard auch noch anderweitig angewandt werden. Jedes Jahr werden in atemberaubender Geschwindigkeit neue Ergebnisse veröffentlicht. Deswegen ist es ungeheuer wichtig, diese Beweise durchsuchen zu können. Wenn alle neuen Abstracts in Lean eingegeben wären, könnte jede Mathematikerin die Datenbank nach einem präzisen mathematischen Objekt abfragen und alles erfahren, was dazu bekannt ist.

Computerforschende könnten eine solche Datenbank als Trainingsplatz für Künstliche Intelligenz nutzen. Mit der präzisen Sprache von Lean können Programme besser umgehen als mit Arbeiten, die in eigenwilligem Englisch verfasst sind.

Ein anderes Ziel der Computerwissenschaft wäre es, einen allgemeinen, automatisierten Theorembeweisenden zu erschaffen – ein Softwaresystem, das seine eigenen Beweise herleitet. Die zunehmende Anwendung von Lean könnte ein wichtiger Schritt zur Automatisierung der Mathematik werden.

Folge VICE auf Facebook, Instagram und Snapchat.