Das lebendige Theorem (German Edition)

einfärbt. Eine gute Idee … Aber wenn man die lokale und die globale Färbung aufeinander abstimmen will, wird es kompliziert, und man muss viele Fälle betrachten: Millionen oder gar Milliarden von Fällen!
    1976 nehmen sich Appel und Haken etwa tausend zu überprüfende Konfigurationen vor und sehen sie alle mit Hilfe eines Computerprogramms durch. Nachdem die Maschine zwei Monate gelaufen war, gelangen sie zu der Schlussfolgerung, dass vier Farben immer ausreichen und lösen damit eine Vermutung, die über hundert Jahre alt ist.
    Die Gemeinschaft der Mathematiker hat sich angesichts dieses Beweises tief gespalten. Hat die Maschine nicht das Denken getötet? Versteht man denn wirklich dieses Argument, das man einem Wesen aus Silizium und integrierten Schaltkreisen zum Fraß vorgeworfen hat? Die Appel-Haken-Anhänger und die Appel-Haken-Gegner stehen sich gegenüber, ohne dass sich ein Konsens abzeichnet.
    Man lernt, mit dieser Polemik zu leben, und wir machen einen zeitlichen Sprung, um zur Jahrtausendwende nach Frankreich zurückzukehren, an das INRIA (Institut national de recherche en informatique et en automatique [nationales Forschungsinstitut für Informatik und Automation]). Georges Gonthier, Experte für Sprachen zur Überprüfung von Beweisen, ist einer der Forscher, die an diesem auf Informatik und Rechnungen spezialisierten Institut angestellt sind. Sein Arbeitsbereich wurde in Europa von einigen schwärmerischen Theoretikern entwickelt, als zur selben Zeit Appel und Haken von sich reden machten. Diese Sprachen überprüfen einen mathematischen Beweis, wie Sie die Festigkeit eines Baumes überprüfen würden, Ast für Ast: Stellen Sie sich einen logischen Baum vor, in den Überlegungen eingeschrieben sind, die zum Gegenstand einer automatischen Überprüfung werden können, nach dem Vorbild einer Rechtschreibprüfung.
    Aber während eine Rechtschreibprüfung sich nur dafür interessiert, ob die Wörter auch richtig geschrieben sind, wird Ihr Programm für Beweisanalyse seinerseits die Kohärenz des Ganzen überprüfen, d.h. dass alles richtig ist.
    Mit der Unterstützung eines Mitarbeiters, Benjamin Werner, beschließt Gonthier, sich an den Beweis des Vierfarbentheorems zu machen, und zwar in einer zu Ehren ihres Schöpfers Thierry Coquand »Coq« genannten Sprache. Im Gegensatz zu den Programmen, die Appel und Haken verwendet haben, ist Coq zertifiziert: Man weiß, dass es keinen Fehler produzieren kann. Und Coq liefert auch nicht wirklich Rechnungen, sondern generiert automatisch den Beweis anhand des Algorithmus, den man eingibt. Gonthier nutzt das aus, um den »lesbaren« Teil des Beweises neu zu schreiben. Auf diese Weise erhält er etwas Einfaches und Leistungsfähiges, etwas Schönes! Ein von einem Menschen zu 0,2% geschriebener Beweis, der von der Maschine zu 99,8% ergänzt wird – aber es sind doch die menschlichen 0,2%, die zählen. Bei Coq weiß man, dass man sich auf den Rest verlassen kann.
    Die Arbeiten von Gonthier und seinen Kollegen geben einen Vorgeschmack auf Prüfsoftware, die in nicht allzu ferner Zukunft automatisch komplexe Programme überprüfen können, die den Start von Raketen, den Flug von Flugzeugen oder die Mikroprozessoren unserer PCs steuern. Was inzwischen bei dem, was vor dreißig Jahren noch ein süßer Traum war, finanziell auf dem Spiel steht, beläuft sich jetzt auf Milliarden von Euros.
    Was den unermüdlichen Gonthier betrifft, so hat er sich gegenwärtig in ein äußerst ehrgeiziges Projekt gestürzt: die Überprüfung bestimmter Klassifikationstheoreme endlicher Gruppen, deren Beweise dafür bekannt sind, dass sie zu den längsten des 20. Jahrhunderts gehören.
    *
    Pour un mot qui clame
    Un mot de travers
    Il y aura des flammes
    Dans tout l’univers
    Les bouches sont grandes
    Pour les beaux discours
    Mais les peaux se vendent
    Les peaux de tambours
    Un jour nos langages
    Parleront de fleurs
    Et du mariage
    Des quatre couleurs
    Sauras-tu comprendre
    Qu’ils parlent d’amour
    Moi je vais t’attendre
    Au pied de la Tour
    En attendant, Caïn chasse toujours Abel
    Mais j’ai construit de mes mains la Tour de Babel
    Für ein Wort
    Das ein verkehrtes Wort hinausschreit
    wird es im ganzen Universum
    Flammen geben
    Die Münder sind groß
    Für schöne Reden
    Aber die Haut wird verkauft
    Die Haut der Trommeln
    Eines Tages werden unsere Sprachen
    Von Blumen sprechen
    Und von der Heirat
    Der vier Farben
    Wirst du verstehen
    Dass sie von Liebe sprechen
    Ich werde auf