Wissenschaftsgegner argumentieren häufig, daß es Beweise nur in Mathematik und Logik gäbe, weshalb zum Beispiel die Evolutionstheorie nicht als bewiesen, sondern bestenfalls als zu einem hohen Grade bestätigt anzusehen sei.
Dem Thema Beweise, besonders dem relativ neuen Thema formale Computer-überprüfte Beweise, widmeten sich mehrere Artikel in der Dezember-Ausgabe der Notices of the American Mathematical Society, worüber ich hier kurz berichten will.
Beweise nach Bourbaki
Ein (mathematischer) Beweis ist die Herleitung der Richtigkeit einer Aussage aus einer Menge von Axiomen mittels klar definierter Regeln.
So kennt man es seit Euklid1.
Wobei: klar definierte Regeln sind jedenfalls nicht die, die wir im Mathematik-Unterricht in der Schule gelernt haben. Denn dort rechnet man ja (zum Beispiel) mit den ganzen Zahlen 1,2,3,… rein “intuitiv”, ohne jemals diese Rechenregeln formal bewiesen zu haben.
Bourbaki hatte 1939 in seinem Lehrbuch zur Mengenlehre einen streng formalen Aufbau der Mathematik (auf Basis der Mengenlehre) dargestellt.
Nur: mit dem Ansatz von Bourbaki ist es (ohne Computer) zwar theoretisch, aber nicht praktisch, möglich, die Mathematik formal zu entwickeln. Selbst wenn man nur elementare zahlentheoretische Tatsachen auf dem Niveau der 1.Grundschulklasse streng nach Bourbaki formal beweisen wollte, bräuchte man (nach Berechnungen von A.R.D.Mathias2) Argumentationsketten aus Billionen von Symbolen. Von anspruchsvolleren Beweisen gar nicht zu reden.
Also: formale Beweise auf der Basis von Bourbaki’s Axiomen sind theoretisch, aber nicht praktisch möglich. Jedenfalls nicht ohne Hilfe von Computern.
Traditionelle vs. formale Beweise
Zwar sagt man immer, daß in der Mathematik jede Behauptung formal bewiesen (also die Behauptung aus den Voraussetzungen mittels der klar definierten Regeln hergeleitet) wird. Aber in Wirklichkeit ist es natürlich schon so, daß mathematische Beweise viele Routinen und Analogieschlüsse benutzen, deren Richtigkeit so selbstverständlich ist, daß man sie nicht formal beweist. Niemand wird sich die Mühe machen, innerhalb eines Beweises noch zu begründen, daß 52/26=2 tatsächlich aus den Axiomen der Arithmetik folgt.
(Wie jeder Mathematiker weiß, gibt es darüber hinaus natürlich auch große stilistische Unterschiede zwischen stärker geometrisch, durchaus auch mit handwaving, argumentierenden Mathematikern und, etwa in manchen Teilen der Algebra, sehr formalen Argumenten. Das wäre aber noch ein anderes Thema, das hier zu weit weg führen würde.)
Deshalb wird in den Notices-Artikeln unterschieden zwischen traditionellen Beweisen und formalen Beweisen.
Traditionelle Beweise, wie sie Mathematiker jeden Tag produzieren, sind, selbst wenn sie sehr streng und formal aussehen, fehleranfällig, weil sie eben doch von Menschen stammen und bei weitem nicht völlig formal sind.
Formale Beweise sind Beweise, in denen wirklich jede Tatsache regelgerecht aus den Axiomen hergeleitet wird. Formale Beweise sind erst seit einigen Jahren, mit Computerhilfe, möglich.
John Harrison von Intel vergleicht in einem der Notices-Artikel diese neue Situation mit der Situation in der Analysis (Differentialrechnung) am Anfang des 19.Jahrhunderts. Newton, Euler etc. war es ja immer bewußt gewesen, daß viele ihrer Rechnungen auf einem unklaren logischen Fundament aufbauen, aber erst im 19. Jahrhundert wurde die Analysis auf die heute gebräuchliche formale Grundlage (ε-δ-Beweise, Grenzwerte, …) gestellt.
Die (langfristige) Perspektive der Notices-Autoren ist offenbar, daß man anstreben soll, in Zukunft alle mathematischen Beweise mit Computerhilfe auf vollständige formale Korrektheit zu überprüfen.
Computer-überprüfte Beweise
Um ein mögliches Mißverständnis zu vermeiden: man erwartet nicht, daß Computer in absehbarer Zeit in der Lage sein werden, mathematische Beweise zu finden. Man muß zunächst einen traditionellen Beweis, also einen von einem Menschen mit mehr und weniger genialen Ideen gefundenen Beweis, vorliegen haben und kann ihn erst dann mit Computerhilfe formalisieren und überprüfen, um ihn zu einem formalen Beweis werden zu lassen. Bei formalen Beweisen handelt es sich also um von (in der Regel genialen) Mathematikern gefundene Beweise, die vom Computer nur überprüft wurden.
(Ein anderes Thema sind Computerbeweise wie beim 4-Farben-Problem oder der Kepler-Vermutung. Hier ging es nicht um die formal vollständige Verifikation, sondern um das Abarbeiten sehr vieler Fallunterscheidungen, die für einen Menschen zu aufwendig gewesen wäre. Diese älteren Computerbeweise waren keine formalen Beweise. Allerdings gibt es für den 4-Farben-Satz inzwischen einen formalen Beweis, an einem formalen Beweis der Kepler-Vermutung wird noch gearbeitet.)
Es gibt inzwischen eine Reihe schwieriger Sätze, zu denen tatsächlich formale Beweise vorliegen. Der erste war 1986 ein Computerbeweis von Gödels Unvollständigkeitssatz. (Dieser besagt, daß es unbeweisbare richtige Sätze gibt. Es hat natürlich eine gewisse Ironie, daß ausgerechnet der Beweis der Unbeweisbarkeit der erste von einer Maschine bewiesene Satz war.) Auch zum 4-Farben-Satz (dem Satz, daß sich jede Karte mit 4 Farben färben läßt) gibt es inzwischen einen vollständigen Computerbeweis (nachdem ja bereits der ursprüngliche Beweis von Appel und Haken 1976 in wesentlichen Teilen auf Computer-Rechnungen basierte, was seinerzeit zu großen Diskussionen führte, nicht zuletzt weil man tatsächlich eine Reihe von Fehlern in Details fand). Dieser Computerbeweis des 4-Farben-Satzes wird in den Notices in einem eigenen Artikel besprochen.
Viel beeindruckender als diese beiden Sätze fand ich einige andere Sätze, die ich nicht unbedingt als leicht formalisierbar angesehen hätte: zum einen gibt es inzwischen eine Computer-Überprüfung zum Selberg-Erdös-Beweis des Primzahlsatzes (dieser gibt eine näherungsweise Formel für die Anzahl der Primzahlen bis zu einer gegebenen Stelle) und zum anderen gibt es Computer-Überprüfungen zu topologischen Sätzen wie dem Jordanschen Kurvensatz oder auch dem Brouwerschen Fixpunktsatz. (Über letzteren und seine Anwendungen hatte ich z.B. in TvF 32,33, 34, 36 und 42 geschrieben.)
Beides sind Sätze, die ursprünglich sehr aufwendige Beweise hatten, für die man inzwischen aber kurze Beweise mittels algebraischer Topologie kennt. Für diese kurzen Beweise muß man aber eben vorher eine Menge Theorie kennen (und diese vielen theoretischen Resultate muß der Computer dann natürlich auch alle erst nachgeprüft haben – hier also die diversen Eigenschaften der Homologiegruppen, die man in beiden Beweisen benötigt.)
Es gibt eine Reihe verschiedener Beweisüberprüfungsprogramme, das erfolgreichste ist wohl HOL Light, dem auch ein Artikel in den Notices gewidmet ist. Es gibt ca. 80 bekannte mathematische Lehrsätze, die mit Computer nachgeprüft wurden. Die meisten Überprüfungen (nämlich mit 17 verschiedenen Programmen) gibt es zum Beweis, daß die Wurzel aus 2 irrational ist. (Nicht sehr überraschend, weil dieser Beweis tatsächlich nicht nur kurz ist, sondern auch nichts weiter als elementare Eigenschaften ganzer Zahlen benutzt.)
Hat man mit den formalen Computer-Überprüfungen nun absolute Sicherheit betreffs der Richtigkeit der bewiesenen Resultate?
Laut Notices macht ein Programmierer etwa 1,5 (Tipp-)Fehler pro Zeile und immerhin 1 Fehler pro 100 Zeilen bleibt unbemerkt. Also, auch bei Computerbeweisen hat man keine absolute Gewißheit. (Mal abgesehen davon, daß Computerfehler möglich sind. Die kann man durch mehrmaliges Laufen auf unterschiedlichen Rechnern zwar praktisch, aber nicht absolut, ausschließen.) Also: Wissenschaftsgegner können auch in Zukunft argumentieren, daß es selbst in der Mathematik keine absolute Gewißheit, sondern nur Grade der Bestätigung gibt.
(PS: ich hoffe mal, daß dieser Artikel genug Fachtermini und vor allem komplexe Sachverhalte enthält, um zu verhindern, daß er womöglich von schleimigen Wissenschaftsgegnern gelesen oder gar zitiert wird.)
1 Am Rande: Als Musterbeispiel streng logischen Schließens gelten ja immer Euklids “Elemente”. Bekanntlich wird dort die elementare Geometrie durch streng logisches Schließen aus wenigen Axiomen hergeleitet. Weniger bekannt ist vielleicht, daß bereits im Beweis der 1. Proposition folgende Tatsache ohne Beweis verwendet wird: zwei Kreise, die jeweils durch den Mittelpunkt des anderen Kreises verlaufen, müssen sich schneiden. Wie im Bild rechts.
Das ist sicher anschaulich klar, aber Euklid hat es eben nicht (aus seinen Axiomen) bewiesen. Und man kann es wohl auch gar nicht aus Euklids Axiomen herleiten. Hilbert hat weitere (Anordnungs-)Axiome hinzugefügt, mit denen sich solche Probleme dann lösen lassen.
Über Euklids Elemente schreibt O’Shea:
Mathematiker und Gelehrte wissen um die Schwachstellen bei Euklid, und im Lauf der Jahrhunderte wurde viel über alternative Axiome oder mögliche Zusätze diskutiert. Das hat Generationen ehrführchtiger Schulmeister nicht davon abgehalten, sich an der majestätischen Ordnung, der Verständlichkeit und der Praktikabilität der “Elemente” zu berauschen und sie vorschnell als die größte Leistung menschlichen Denkens zu bejubeln. Einem nachdenklichen Schüler könnten sie jedoch eher kapriziös als rational vorkommen.
Man sollte nicht vergessen, daß alle Erkenntnise der Mathematik, auch wenn sie als ewig gültig und von der menschlichen Gesellschaft unabhängig hingestellt werden, in Wirklichkeit in bestimmten kulturellen und sozialen Kontexten gewonnen und weitergegeben werden. Einige argumentieren beispielsweise, die Griechen hätten den Beweis erfunden, um die Aussagen der ägyptischen und babylonischen Mathematik verstehen zu können, ohne Zugang zu dem Kontext zu haben, in dem deren Erkenntnisse gewonnen und angewandt wurden.
2Die Berechnungen von A.R.D.Mathias findet man in seiner Arbeit A Term of Length 4,523,659,424,929. Seine Inhaltsangabe dieser (stellenweise recht polemisch geschriebenen) Arbeit: “A calculation of the number of symbols required to give Bourbaki’s definition of the number 1; to which must be added 1,179,618,517,981 disambiguatory links. The implications for Bourbaki’s philosophical claims and the mental health of their readers are discussed.“
Kommentare (45)