Ein kontroverser Beweis in der Mathematik – einer, der das Fachgebiet seit über einem Jahrzehnt spaltet – könnte endlich von einem ungewöhnlichen Richter entschieden werden: einem Computerprogramm. Der Kern der Debatte dreht sich um Shinichi Mochizukis Versuch aus dem Jahr 2012, die ABC-Vermutung zu lösen, ein seit langem bestehendes Problem, das tief in der fundamentalen Natur von Zahlen verwurzelt ist.
Die ABC-Vermutung basiert auf einer täuschend einfachen Gleichung mit drei ganzen Zahlen: a + b = c. Es legt spezifische Regeln fest, die regeln, wie sich die Primzahlen, aus denen diese ganzen Zahlen bestehen, verhalten müssen. Die Lösung dieses scheinbar grundlegenden Problems könnte tiefgreifende Einblicke in die Mathematik ermöglichen und möglicherweise Auswirkungen auf andere berühmte Vermutungen wie Fermats letzten Satz haben.
Mochizuki, Professor an der Universität Kyoto in Japan, präsentierte seinen Beweis in einem komplexen Rahmen, den er erfunden hatte und der als interuniverselle Teichmüller-Theorie (IUT) bezeichnet wird. Die schiere Formalität und Unklarheit der IUT-Theorie machte sie jedoch für die meisten Mathematiker, die versuchten, seine Arbeit zu überprüfen, weitgehend unverständlich. Die anfängliche Begeisterung wich der Frustration, als Experten darum kämpften, die Feinheiten zu entschlüsseln.
Als zusätzliches Öl im Jahr 2018 identifizierten zwei prominente deutsche Mathematiker – Peter Scholze und Jakob Stix – einen möglichen Fehler in Mochizukis Beweis. Mochizuki entgegnete ihrem Argument, und ohne ein übergeordnetes Gremium zur Schlichtung mathematischer Streitigkeiten spaltete sich das Feld in zwei Lager: diejenigen, die weitgehend die Mainstream-Ansicht akzeptierten (die von den meisten Mathematikern unterstützt wurde), und eine kleinere Gruppe, die sich mit Mochizuki und seinem Institut in Kyoto verbündete.
Jetzt schlägt Mochizuki einen Weg nach vorne durch Formalisierung vor – indem er seinen Beweis von einer für Menschen lesbaren mathematischen Notation in Lean umwandelt, eine Computerprogrammiersprache, die speziell für strenge mathematische Verifizierung entwickelt wurde. Dieser Prozess könnte es Computern möglicherweise ermöglichen, die Konsistenz seiner Argumente automatisch zu überprüfen und so ein beispielloses Maß an Objektivität zu erreichen.
Mochizuki glaubt, dass Lean in einzigartiger Weise in der Lage ist, die komplexen sprachlichen und konzeptionellen Hürden zu überwinden, die den Fortschritt beim Verständnis der IUT-Theorie blockiert haben. Er betrachtet es als ein Werkzeug, um die mathematische Wahrheit von den potenziellen Vorurteilen zu befreien, die der menschlichen Interpretation innewohnen.
Während einige Experten wie Kevin Buzzard vom Imperial College London dies als eine vielversprechende Richtung sehen, erkennen sie auch die gewaltige Herausforderung an, die vor uns liegt. Die Formalisierung der IUT-Theorie würde die Übersetzung großer Mengen komplizierter Gleichungen in die Lean-Syntax erfordern – ein Unterfangen, das mit einigen der größten Formalisierungsprojekte aller Zeiten vergleichbar wäre. An solchen Bemühungen sind oft engagierte Teams aus Mathematikern und Programmierern beteiligt, die sich über Monate oder sogar Jahre erstrecken.
Johan Commelin von der Universität Utrecht in den Niederlanden ist zwar vorsichtig optimistisch, betont aber, dass der Erfolg von Mochizukis nachhaltigem Engagement abhängt. Er warnt davor, dass das Projekt, wenn es vorzeitig aufgegeben wird, einfach zu einem weiteren Kapitel in einer langwierigen Saga werden könnte, die von ungelösten Streitigkeiten geprägt ist.
Commelin weist darauf hin, dass selbst im Erfolgsfall auch bei computerverifiziertem Code Meinungsverschiedenheiten über die Interpretation bestehen bleiben könnten. Lean löst möglicherweise logische Widersprüche, unterdrückt jedoch nicht unbedingt alle philosophischen oder konzeptionellen Unterschiede rund um Mochizukis Werk.
Letztendlich bietet die Formalisierung zwar einen Hoffnungsschimmer für die Lösung dieser anhaltenden mathematischen Pattsituation, es bleibt jedoch abzuwarten, ob sie die tief verwurzelten Komplexitäten und unterschiedlichen Perspektiven überwinden kann, die die Debatte über den ABC-Vermutungsbeweis geprägt haben.
