[…]
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.)
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)