Zahlentheoretiker: Große Beweise könnten alle falsch sein

Der Grund für die Annahme von Kevin Buzzard: Viele Beweise sind so umfangreich, dass sie niemand bis ins kleinste Detail durchgearbeitet und verstanden hat. Als Beispiel führt er den Beweis für Fermats letzten Satz an, der 1637 vorgeschlagen wurde und einst im Guinness Buch der Rekorde als das "schwierigste mathematische Problem" der Welt angesehen wurde. Buzzard: "Ich glaube, dass kein Mensch, ob lebendig oder tot, alle Details des Beweises von Fermats letztem Satz kennt. Aber die Gemeinschaft akzeptiert den Beweis trotzdem, weil 'die Ältesten' angeordnet haben, dass der Beweis in Ordnung ist."

Buzzard sagt, dass ein Beweis dann allgemein akzeptiert wird, wenn einer oder mehrere besonders rennomierte Mathematiker (Buzzard nennt sie "die Ältesten", englisch "the elder") den Beweis als korrekt ansieht. Beweise neueren Datums können auf 20 oder mehr ältere Beweise aufbauen. Jeder davon könnte auf 1000 Seiten komplexer mathematischer Beweisführung beruhen. Finden die Ältesten das Ergebnis gut – auch ohne die Beweistführung nachvollzogen zu haben – kann das ungeprüfte Ergebnis als Grundlage für weitere Beweise dienen.

Einen Ausweg aus diesem Dilemma sieht Buzzard in mathematischer Software, welche die Überprüfung von Beweisen erlaubt. Er nennt dafür das Beispiel Lean von Microsoft Research, das er selbst nutzt. Die Beweisführung muss dafür Zeile für Zeile in die Programmiersprache von Lean übersetzt werden. Das dauert und die Software akzeptiert keine Fehler. Doch das Ergebins belohnt die Arbeit. Je mehr Beweise im Format von Lean vorliegen, desto mehr davon können in einer durchsuchbaren Datenbank hinterlegt werden. Letztlich kann man die Datenbank sogar nutzen, um eine KI damit zu trainieren.

Und Buzzard ist damit nicht alleine: Das Helix Center Manhattan will am 5. Oktober eine Diskussionsrunde über die Automatisierung der Mathematik veranstalten, die live von YouTube und seiner Website übertragen wird. Michael Harris, Professor für Mathematik an der Columbia University und Kollege von Buzzard, will am Forum teilnehmen. Harris ist besorgt, dass die Informatiker und Technologieunternehmen, die Mathematik automatisieren wollen, nicht die gleichen Motivationen haben wie Mathematiker. So wollen beispielsweise Informatiker die Technologie hinter Lean nutzen, um sicherzustellen, dass Programme fehlerfrei sind. Unternehmen wollen Gewinne erzielen. Mathematiker wie Buzzard wollen nur rechnen. Harris: "Eine Sache, die ich vorhersagen kann, ist, wenn wirklich kluge Leute wie Thomas Hales (Mathematikprofessor an der University of Pittsburgh) und Buzzard weiterhin in diese Richtung denken, dann wird etwas Interessantes dabei herauskommen; es mag keine KI sein, aber es kann ganz neue Zweige der Mathematik oder ganz neue Denkweisen sein".

Den kompletten englischsprachigen Beitrag "Number Theorist Fears All Published Math Is Wrong" lesen Sie hier.