Früher war alles besser – oder zumindest einfacher.

Über diese Welt im Wandel konnte ich mich einmal mit Shiing-Shen Chern unterhalten, einem der großen Vertreter der Geometrie des 20. Jahrhunderts. Er beschrieb mir, wie er seine eigene, eigenständige Arbeit aufnehmen konnte, als er zu Beginn seiner Karriere die Arbeit von Heinz Hopf über die Hopf-Faserungen las und sich an der Grenze der damaligen Mathematik wiederfand. Nun sind Hopfs Gedanken wundervoll, aber relativ leicht zu untersuchen. Im beginnenden 21. Jahrhundert ist es in der Regel deutlich schwieriger, an die Grenze der Mathematik vorzustoßen. Allein die Vorstellung, neben anderen die Ideen Grothendiecks bezwingen zu müssen, wenn man in der algebraischen Geometrie und der Arithmetik arbeiten will!

i-4c6c1131c26b5ae94e09498a242c874c-4830hopffibration1.jpg

Hopffaserung – Copyright Dimensions

Ruelle berichtet, daß in den 60er Jahren Mathematiker kritisiert wurden, wenn sie Ergebnisse von Kollegen verwendeten, ohne sie selbst überprüft zu haben. Deligne meinte in den 70ern, ihn interessiere Mathematik, die er selbst bis ins letzte Detail nachvollziehen könne, keine computergestützten oder extrem langen Beweise. Computergestützte oder extrem lange Beweise sind heute aber alltäglich geworden.

Ruelle diskutiert in diesem Zusammenhang einen Zerfall “moralischer Werte” in der Mathematik. Insbesondere erwähnt er einen Artikel von Jaffe-Quinn und die Debatte über Thurstons Beweis der Geometrisierungs-Vermutung für Haken-Mannigfaltigkeiten:

Thurstons Programm beanspruchte damit ein großes Gebiet der Mathematik, ohne dabei allerdings Beweise zu liefern, welche von Kollegen überprüft werden könnten. Letztlich erschwerte er anderen Mathematikern das Arbeiten in diesem Bereich: Man erntet keine großen Lorbeeren für den Beweis eines bereits formulierten Theorems […]

Hier muß man vielleicht ergänzen, daß das so nicht zutrifft. Die Mathematiker, die vollständige Beweise zu Thurstons Theoremen ausarbeiteten, haben damit durchaus Lorbeeren geerntet: McMullens Ausarbeitung eines fehlenden Details im Beweis für Haken-Mannigfaltigkeiten erschien 1990 in “Inventiones Mathematicae” (und brachte ihm 1998 die Fields-Medaille), Otals Beweis wurde in “Asterisque” veröffentlicht. Bonahons Habilitation, in der “nur” 2 Kapitel aus Thurstons Vorlesung aufgearbeitet wurden, erschien als 87-seitiger Artikel in den renommierten “Annals of Mathematics”, auch z.B. der Beweis des Orbifold-Satzes wurde in “Annals of Mathematics” veröffentlicht etc.pp.

Es gibt übrigens eine Erwiderung von Thurston auf den Jaffe-Quinn-Artikel. Er führt dort aus, daß seine früheren Arbeiten über Blätterungen, z.B. der (vollständige) Beweis des Existenzsatzes, dieses Gebiet ‘getötet’ hätten in dem Sinne, daß diese Fragen damit beantwortet und abgeschlossen waren und kein forschender Mathematiker sich mehr mit seinem Beweis beschäftigte. Dagegen habe er später bei der Geometrisierungsvermutung keine vollständigen Beweise mehr aufgeschrieben(“By concentrating
on building the infrastructure and explaining and publishing definitions and ways of thinking but being slow in stating or in publishing proofs of all the “theorems” I knew how to prove, I left room for many other people to pick up credit.”
) und damit erreicht, daß dieses Thema sich zu einem sehr aktiven Forschungs-Gebiet entwickelte.

i-882a9e8675cdbf5a0d59d1ab83a7edd7-proofprogress.png

W.Thurston: On proof and progress in mathematics

(Vgl. dazu auch David Corfield: “Wittgenstein and Thurston on understanding” mit weiteren Links.)

Außerdem diskutiert Ruelle in diesem Kapitel noch die Rolle von Computern in der mathematischen Forschung.
Zum einen natürlich auf einer heuristischen Ebene: Riemann nahm lange Berechnungen von Hand vor, um einige Gedanken zu überprüfen; sicherlich hätte er sich gefreut, einen schnellen Computer zur Hand zu haben.” Auch Ruelle selbst hatte in seiner Arbeit mit Eckmann über seltsame Attraktoren Computer-Experimenten benutzt.
Zum anderen für rigorose Beweise: exakte Berechnungen mit ganzen Zahlen, Programmierung logischer Operationen wie beim Beweis des 4-Farben-Satzes, und exakte Berechnungen mit reellen Zahlen mittels Intervallarithmetik: als Beispiel erwähnt er eine unveröffentlichte Arbeit von Oscar Lanford, in der mit Intervallarithmetik (und einem 200 Seiten langen Computercode) bewiesen wird, daß bestimmte unendlich-dimensionale Mannigfaltigkeiten sich transversal schneiden.

Mit der zunehmenden Länge der Beweise wird auch das Problem der Fehler in der Mathematik immer schwerwiegender, ganz gleich, ob nun Computer verwendet werden oder nicht.

[…]

Wie schwerwiegend das Problem von Fehlern oder Lücken sein kann, wird deutlich, wenn wir uns nochmals das Theorem der Klassifikation endlicher einfacher Gruppen anschauen. Der Beweis dieses Theorems füllt Tausende von Seiten aus der Feder vieler Autoren und wurde zum Teil computergestützt geführt. Das Theorem gilt seit ungefähr 1980 als “moralisch” bewiesen, wobei einzelne Teile noch niedergeschrieben werden mußten. Der Beweis war also lückenhaft, doch die Lücken wurden von Fachleuten nicht als gravierend angesehen. Immerhin aber erwies sich eine dieser Lücken als so schwerwiegend, dass (im Jahr 2004) weitere 1.200 Seiten Beweisführung notwendig wurden.

Jedenfalls hat die Mathematik ihre “alten Anforderungen an die Rigorosität” nicht aufgegeben (“Grundsätzlich lässt sich sagen, dass gute Mathematiker, die in einem bestimmten Bereich arbeiten, wissen, wie zuverlässig die dazu veröffentlichte Literatur ist.”), auch wenn der Stil der Mathematik sich geändert hat und sich weiter ändern wird.
Ruelle diskutiert zum Schluß noch computergeprüfte formale Beweise. (Darüber hatten wir hier schon einmal geschrieben.) Der meistbenutzte Theorembeweiser HOL Light besteht aus weniger als 500 Zeilen Computercode (ist also hoffentlich fehlerfrei), mit ihm wurden zum Beispiel der Beweis des Primzahlsatzes oder des 4-Farben-Satzes überprüft. (Der Beweis des 4-Farben-Satzes wurde mit Coq überprüft.)

i-41adb590839297c9f3e6e48c08855449-hol.png

Bedienungsanleitung für Theorembeweiser HOL Light

Ruelle: Wie Mathematiker ticken
1 Wissenschaftliches Denken
2 Was ist Mathematik?
3 Das Erlanger Programm
4 Mathematik und Ideologie
5 Die Einheitlichkeit der Mathematik
6 Ein kurzer Blick auf algebraische Geometrie und Arithmetik
7 Mit Alexander Grothendieck nach Nancy
8 Strukturen
9 Die Rechenmaschine und das Gehirn
10 Mathematische Texte
11 Ehrungen
12 Die Unendlichkeit: Nebelwand der Götter
13 Fundamente
14 Strukturen und die Entwicklung von Konzepten
15 Turings Apfel
16 Mathematische Erfindung: Psychologie und Ästhetik
17 Das Kreistheorem und ein unendlich-dimensionales Labyrinth
18 Fehler!
19 Das Lächeln der Mona Lisa
20 „Tinkering” und die Konstruktion mathematischer Theorien
21 Mathematische Erfindung
22 Mathematische Physik und emergentes Verhalten
23 Die Schönheit der Mathematik

Kommentare (3)

  1. #1 frederik
    1. Juli 2010

    Ich persönlich habe noch nichts davon gehört, dass der 4-Farben-Satz in HOL formalisiert wurde. Es gibt jedoch einen Formalen Beweis in Coq von Georges Gonthier über den u.a. ein Artikel in den Notices der AMS erschienen ist: https://www.ams.org/notices/200811/

  2. #2 frederik
    1. Juli 2010

    Ups, dazu gab es hier ja scheinbar sogar mal einen Beitrag, der unter diesem verlinkt ist…

  3. #3 Thilo
    1. Juli 2010

    Richtig, der Beweis nutzt Coq. Ich hab’s jetzt auch oben im Text korrigiert.
    https://www.ams.org/notices/200811/tx081101382p.pdf