Mathematik Das rechnende TierSeite 3/3

Wieso sollte ausgerechnet die Mathematik vom (gesellschaftlichen) Phänomen der Segregation verschont bleiben?

Des permanente „Höher, schneller, weiter!“ in unserer Gesellschaft verursacht allenthalben mindestens zwei „Kollatteralschäden“. Der erste besteht darin, dass die Wettbewerbssieger schlussendlich unter sich sind (und bleiben), weil ihnen kaum noch jemand (zu) folgen (ver-)mag – schöne Grüße von hier aus an ilabernet und Dr. Wolff. Der zweite basiert auf dem soeben genanten Umstand und wird im vorliegenden Beitrag beschrieben: An der jeweiligen Grenze wird’s imaginär und unkontrollierbar. Nicht schön, aber unter der beschriebenen Prämisse wohl kaum zu ändern.

So ist er nun einmal, der Mensch, und so wird er bleiben. Beweisen kann ich diese These zwar nicht (bin schließlich kein Mathematiker), aber: Was wollen wir wetten?

Die zunehmend schwierige Beweislage ist sicher ein Problem für die Zunft der Mathematiker. Aber hat das Auswirkungen auf den Fortgang der Erkenntnis in Wissenschaften, die die Mathematik als Hilfswissenschaft benötigen?
Vielleicht kann die Konsequenz dieses Problems jemand vom Fach einmal einen Mathematiklaien erklären?

Tippfehler: das Monster hat 808017424794512875886459904961710757005754368000000000
Elemente, also etwa 10^54, und nicht nur 1054.

Die Anzahl der Elemente (Maechtigkeit) des Monsters ist natuerlich ungefaehr 10E54 und nicht 1054. Die genaue Maechtigkeit dieser Gruppe kann hier nachgelesen werden:
http://mathworld.wolfram....

Schon Wittgenstein hat von einem Beweis gefordert,daß er übersichtlich sein solle. Übersichtlich in dem Sinne, daß der Mathematiker ihn in seiner Gänze erfassen kann (was auch immer das heißen mag).
Daß ein Beweis Lücken haben oder sogar falsch sein kann, ist nun beim besten Willen auch nicht neu. Wahrscheinlich hat jeder Mathematiker (es gibt sehr berühmte Beispiele) einmal einen fehlerhaften Beweis vorgelegt. Dies lag dann meistens daran, dass Begriffe verwendet wurden, die nicht exakt genug definiert waren, oder in ihrer Bedeutung unklar waren. Die Logik und Mengenlehre des frühen 20. Jahrhunderts hat gerade versucht diese Unklarheiten zu beseitigen. Ein Ansatz (der wirkungsmächtigste) war der einer vollkommenen Durchformalisierung der Mathematik. Ziel war es nicht den Mathematiker auf Formalisierung zu trimmen, sondern ihm eine gewisse Grundlagensicherheit in Bezug auf seine Arbeiten zu geben. Man kann Beweise der Gruppentheorie, formal aufschreiben. Doch diese sind dann gerade nicht mehr überschaubar. Die meisten Mathematiker gehen (wenn sie überhaupt darüber nachdenken) davon aus, dass sich jeder Beweis wahrscheinlich formalisieren läßt. Das sie es nicht tun eröffnet die Möglichkeit von Irrtümern. An dieser Stelle können Computer tatsächlich Abhilfe schaffen. Jedoch werden sie (das ist meine Überzeugung), in naher Zukunft keinen interessanten mathematischen Satz finden. Denn das ist der entscheidende Unterschied: Die Frage nach dem Beweis ist meines Erachtens zweitrangig. Viel wichtiger ist die Formulierung von Definitionen und vor allen Dingen Sätzen. Unbewiesene Vermutungen sind immer noch (siehe Preisgelder) die größte Antriebsfeder innerhalb der Mathematik. Diese Sätze zu formulieren erfordert Einsicht oder auch ein gewisses Maß an Intuition. Das kann (noch) kein Computer. Der Beweis des Vier-Farben-Satzes ist ja nicht alleine die Leistung eines Computers. Der Nachweis, dass sich das Problem in genau so und so viele Teilprobleme aufsplitten läßt ist ja vermutlich (ich weiß es nicht) von Menschenhand gemacht worden. Der Computer hat an dieser Stelle nur die "Drecksarbeit" übernommen. So wie ich das sehe, würde ich einen Beweis tausendmal lieber einem Computer anvertrauen als einem Menschen. Die Forderung nach Übersichtlichkeit, hat nämlich nur einen Zweck: Sie soll garantieren, daß keine Fehler gemacht werden. An dieser Stelle ist Mathematik wie jede Wissenschaft auf Reproduzierbarkeit bedacht. Jede Veröffentlichung in mathematischen Zeitschriften wird ja von mehreren Gutachtern durchgelesen, gerade weil man sich auf den menschlichen Kopf nicht verlassen kann. Das selbe Prinzip macht einen Beweis durch Computer legitim. Er ist wiederholbar und damit "sicher". Was vor allen Dingen verwirrend ist, ist die Vorstellung von der Mathematik als purer Logik. Um Gottes Willen, gerade das ist sie nicht. Sie ist zu einem gut Teil Konvention. Jedweder Platonismus ist an dieser Stelle eine bequeme Ausrede, weil er einem ein Gefühl von Sicherheit verschafft, das so nicht existiert.

Ein kurioser Artikel, der versucht, ein zugegebenermassen schwieriges Grundlagengebiet der Mathematik durch eine Mischung von launigen Kommentaren ("Rechenknecht") und
Oberfl"achlichkeiten f"ur das breite Publikum verdaulich zu machen.

Der Idee, mathematische Beweise auf formalisierte Argumentationen ("formale Beweise") zur"uckzuf"uhren, die
von der wichtigen, aber oft tr"ugerischen Intuition unabh"angig sind, ist ein uralter Menschheitstraum. Er reicht von Aristoteles "uber Leipnitz bis eben zu Forschern wie Hales. Informelle Beweise oder Lehrbuchtexte sind zur Kommunikation nicht "uberfl"ussig, aber wenn man "uber Details streitet, sind formale Beweise eben die Referenzgr"o"sse. Wenn die "g"angige Meinung" das tats"achlich wei"ss, f"ande ich das gro"ssartig und keinesfalls "naiv".

Nun ist es richtig, dass der Begriff der formalen Beweisbarkeit prinzipielle Grenzen hat. Siehe Goedel.
Weiterhin ist richtig, das vollst"andig formale Beweise
aufw"andig und aus praktischen Gr"unden oft undurchf"uhrbar sind. Siehe Monsterbeweise.
Zudem ist richtig, das das Know-how "uber Logik unter
Mathematikern in den letzten Jahrzehnten teilweise abgenommen hat (man kann renommierten Mathematikprofessoren begegnen, die einen Beweis nicht formal aufschreiben, nur verstehen k"onnen; ins Bild passt auch, da"ss ber"uhmte Logiklehrst"uhle in Deutschland zur Zeit nicht wieder von
Logikern, sondern von angewandten Mathematikern wiederbesetzt werden).

Ob diese Schwierigkeiten tats"achlich zu "Krisen" in
"der Mathematik" oder auch nur im mathematischen Forschungsbetrieb gef"uhrt haben, wie Filosofen oft und gern behaupten, sei einmal dahingestellt.

Die Fakten sehen anders aus: Mir ist kein
praktisch relevantes Beweisprojekt bekannt, das
an der Unvollst"andigkeit eines Kalk"uls gescheitert w"are.
Die schiere Gr"osse von formalen Beweisen und Beweisarchitekturen zeugt von der Notwendigkeit der
Zusammenarbeit von Forschungscommunities, ja, aber gerade die m"oglich gewordene Konsistenzpr"ufung durch Computer kann hier einen entscheidenden Unterschied machen (auf
diese Weise hat man immerhin das Problem der menschlichen DNA-Entschl"usselung geknackt). Der R"uckgang der Logik in der Mathematik kann auch etwas mit der historischen Zerschlagung von Zentren wie G"ottingen und einer praktisch motivierten Neuansiedlung der Logik in der Informatik zu tun haben.

Ein Wort noch zu "dem Computer" und dem "Computerbeweis".
Hier geht's in dem Artikel mangels Unterscheidungssch"arfe ziemlich durcheinander. Der Computer wird einesteils genutzt, um Probleme zu enumerieren und zu checken.
Sowohl gegen die algorithmische Seite (werden tats"achlich alle Probleme aufgez"ahlt?) als auch die Implementierungsseite (macht das kryptische Programm in einer kryptischen Programmiersprache wie C wirklich das, was es soll?) hat es berechtigte Kritik an dem urspr"unglichen Appel/Haken "Computerbeweis" gegeben. Und eine notwendige Methodendiskussion. Aber eine "Krise" ist das eben nicht. Zum anderen wird der Computer verwendet, um nachzupr"ufen, ob in einem formalen Beweis jeder einzelne Beweisschritt "stimmt", also einer Anwendung einer Regel des zugrundegelegten Kalk"uls entspricht.
Zweifel gegen solche Nachpr"ufungen, die routinem"a"ssig auf verschiedenen Rechnern immer wieder mit der Pr"azision eines physikalischen Experiments wiederholt werden k"onnen, sind eher hypothetischer Natur. Inzwischen hat Georges Gonthier einen Beweis f"ur das Vier-Farben-Problem in letzterem Sinn vorgelegt, und Hales Monsterbeweis ist inzwischen auch ueber
weite Teile mit Systemen wie HOL-light oder Isabelle
gepr"uft worden.

Zusammenfassend m"ochte ich sagen: Ich sehe durchaus so etwas wie eine Kulturrevolution am Horizont "der Mathematik", sei es in Hinblick auf die R"uckbesinnung auf Grundlagen in ihrem Selbstverst"andnis
oder sei es durch den verst"arkten Einsatz von Computern im mathematischen Forschungsbetrieb.
Einen popul"arwissenschaftlichen Artikel, der diese spannende Entwicklung allgemeinverst"andlich aufarbeitet, habe ich noch nicht gesehen. Auch nicht in "Der Zeit".

Dr. Burkhart Wolff
ETH Z"urich