Er ist vielleicht der berühmteste mathematische Satz nach dem Satz des Pythagoras. Im Volksmund wird er Fermats letzter Satz genannt, benannt nach dem Amateurmathematiker Pierre de Fermat, der sich im 17. Jahrhundert einen Sport daraus machte, Gelehrte wie René Descartes mit unbewiesenen Behauptungen auf die Palme zu bringen. Descartes gilt als Begründer der analytischen Geometrie und ist bekannt für seinen philosophischen Beweis seiner eigenen Existenz in Form des Ausspruchs "Ich denke, also bin ich".

Doch Descartes war weder der einzige Mensch auf der Welt noch der einzige Mensch, der gut im Nachdenken war. Letzteres machte ihm durchaus zu schaffen, wenn es um Pierre de Fermat ging. Fermat genoss es, Gelehrte wie Descartes mit seiner Klugheit zu beeindrucken, obwohl er kein professioneller Wissenschafter war, sondern Richter. Das hinderte ihn nicht daran, bahnbrechende mathematische Ergebnisse zu erzielen. Manchmal machte er sich nicht die Mühe, die Beweise für seine Entdeckungen anzuführen, und überließ lieber seinen Kritikern die Arbeit.

Die Beweise für Fermats Behauptungen waren zuweilen äußerst schwer zu finden. Im Fall von Fermats letztem Satz, um den es hier geht, dauerte die Suche nach dem Beweis über 350 Jahre. Er wurde erst im Jahr 1993 vom britischen Mathematiker Andrew Wiles gefunden, als letzter der fehlenden Beweise, was auch der Ursprung seines Namens ist und Stoff für eine faszinierende Mathematikgeschichte, die im Bestseller "Fermats letzter Satz" des Wissenschaftsjournalisten Simon Singh verarbeitet wurde.

Die Geschichte ist also eigentlich seit den 1990er-Jahren abgeschlossen. Doch der Satz birgt nach wie vor offene Fragen. Um sie zu beantworten, soll der Beweis nun in einen Computer gefüttert und dort erneut überprüft werden.

Von Quadraten und Kuben

Fermats letzter Satz hat neben seiner Berühmtheit noch etwas anderes mit dem Satz des Pythagoras gemein. Er ist eine verallgemeinerte Variante von Ersterem. Während der Satz des Pythagoras sich mit Quadratzahlen beschäftigt, die sich als Summe von Quadratzahlen darstellen lassen, geht es bei Fermat um höhere Potenzen. Genauer gesagt um das Fehlen derselben, wenn es um ganze Zahlen geht.

Beginnen wir mit Pythagoras: Es gibt zahlreiche ganzzahlige Lösungen für diesen Satz, die Pythagoreische Tripel genannt werden. Doch sobald die Quadrate in der Formel durch höhere Potenzen ersetzt werden, wird die Sache komplizierter. Wer nach ganzen Zahlen sucht, die diese Gleichungen erfüllen, wird keine finden. Fermat vermutete einst, dass es keine gibt. Er behauptete sogar, das beweisen zu können.

Das geht aus einer berühmten Notiz hervor, die er an den Rand seines Lieblingsmathematikbuchs kritzelte, eine Ausgabe des Standardwerks des altgriechischen Mathematikers Diophant von Alexandria. Fermat spricht von einem eleganten Beweis, den er gefunden habe, den er aber aus Platzmangel nicht notiere.

Hunderte Seiten Eleganz

Wie dieser Beweis ausgesehen haben könnte, ist unklar. Sicher ist, dass der Beweis von Wiles nicht auf der Buchseite von Fermats Diophant Platz gefunden hätte. Er ist mehrere Hundert Seiten stark und beweist eigentlich einen allgemeineren Zusammenhang über sogenannte elliptische Kurven, aus dem dann quasi nebenbei auch die Behauptung von Fermats letztem Satz folgt.

Derart umfangreiche Beweise werden in letzter Zeit immer häufiger, was zu verschiedenen Problemen führt. So wird etwa über einen monumentalen Beweis des japanischen Mathematikers Shin'ichi Mochizuki nach wie vor gestritten. Die Fachwelt geht eher davon aus, dass er nicht korrekt ist, doch aufgrund seines Umfangs und seiner Schwierigkeit herrscht darüber noch keine vollständige Übereinkunft.

Auch Andrew Wiles hätte beinahe dieses Schicksal ereilt. Als er nach siebenjähriger Arbeit im Stillen seinen Beweis präsentierte, wurde prompt eine Lücke entdeckt. Statt wie Mochizuki auf stur zu schalten und den Streit auf eine persönliche Ebene zu heben, machte Wiles sich erneut an die Arbeit und konnte die Lücke schließen.

Computer als Hilfsmittel

In solchen Situationen könnten künftig ausgerechnet Computer Abhilfe schaffen. Zwar wurde das Konzept des Computers einst geschaffen, um theoretisch die Lösbarkeit von Mathematikproblemen zu untersuchen, doch das Finden von Beweisen selbst galt bis vor kurzem als urmenschliche Fähigkeit, die wie die Poesie echte Inspiration voraussetzte.

Seit einigen Jahrzehnten verschwimmt diese Grenze zunehmend. Immer mehr Beweise nützen auch Computermethoden. Als erstes Beispiel gilt der Vier-Farben-Satz, wonach vier Farben ausreichen, um die Länder einer Landkarte so zu färben, dass niemals zwei gleiche Farben aneinandergrenzen. Er lässt sich in hunderte Spezialfälle zerlegen, bei deren Prüfung Software zum Einsatz kam. Während der Wert eines von ChatGPT geschriebenen Gedichts durchaus infrage gestellt werden kann, ist an einem von Computern durchgeführten mathematischen Beweis nicht das Geringste auszusetzen, sofern nur seine Korrektheit hinlänglich nachvollziehbar ist.

Derweil geht es beim Einsatz von Computern in der Mathematik nicht immer darum, Beweise zu erbringen. Es genügt, wenn sie diese überprüfen. Das erwies sich schon in der Vergangenheit als erfolgreich, etwa in dem außergewöhnlichen Fall des mathematischen Gottesbeweises des großen Logikers Kurt Gödel, in dem sich ein Fehler versteckte, der von einer Software entdeckt wurde.

Doch Gödels Gottesbeweis fasst nur etwa eine Seite. Der Beweis von Wiles ist für Computermethoden eine riesige Herausforderung. Dieser stellt sich nun ein Team um den Mathematiker Kevin Buzzard vom Imperial College London. Er plant, den Beweis in die Programmiersprache Lean zu übertragen, die speziell für mathematische Aussagen konzipiert ist.

Der Computerbeweis soll sich dabei nur grob an dem von Wiles orientieren. Dass eine Übertragung überhaupt gelingen kann, ist nur der Weiterentwicklung der Computermethoden zu verdanken. "Vor zehn Jahren hätte dies noch unendlich viel Zeit in Anspruch genommen", sagt Buzzard gegenüber dem Magazin "New Scientist". Die kommenden fünf Jahre will er seinen Unterricht an der Universität zurückstellen und sich ganz dieser Aufgabe widmen. Eine Skizze der Formalisierung des Beweises soll schon im April vorgestellt werden. Die wissenschaftliche Gemeinschaft, die mit Lean arbeitet, kann sich dann beteiligen und die Formalisierung einzelner Passagen übernehmen. (Auch Sie sind hier gemeint, liebe STANDARD-Leserin, lieber STANDARD-Leser mit Lean-Fähigkeiten!)

Andere Fachleute halten das Vorhaben für zu ambitioniert, fünf Jahre seien zu wenig dafür. Dennoch sei die Arbeit sehr wertvoll. Die dort entwickelten Methoden würden sich auch für andere Aufgaben nutzen lassen.

Gab es den Beweis?

Ob der Beweis, von dem Fermat sprach, je existierte, ist fraglich. Das findet in der Tatsache Niederschlag, dass Fermats "Satz" lange Zeit auch Fermat-Vermutung genannt wurde. Nach dieser Logik müsste Fermats letzter Satz eigentlich "Satz von Wiles" heißen, was eine schöne Anerkennung für den Briten wäre, der 2016 erst mit gehöriger Verspätung den Abelpreis für seine Arbeit erhielt, nachdem er am Alterslimit für die Fields-Medaille nur knapp gescheitert war. Die Fieldsmedaille wird nur an Forschende bis zu einem Alter von 40 Jahren verliehen, um zu verhindern, dass einander alternde Forscher gegenseitig Preise zuschanzen.

Ausschließen lässt sich nicht, dass Fermat tatsächlich einen Beweis besaß. Bei der Suche danach könnten künftig ebenfalls Computermethoden helfen. Erst kürzlich schnitt ein Algorithmus, der ein etabliertes Beweisprogramm mit KI-Methoden kombinierte, bei der Geometrieolympiade so gut ab wie die besten menschlichen Teilnehmerinnen und Teilnehmer.

Mehr noch: Der Algorithmus fand für eines der Probleme einen Beweis, der bislang in der Literatur nicht beschrieben worden war. Computer können neuerdings also auch neue mathematische Zusammenhänge finden und so vielleicht helfen, die letzte offene Frage um Fermats letzten Satz zu beantworten. (Reinhard Kleindl, 1.4.2024)