Das Heidelberg Laureate Forum hat begonnen. Seit drei Jahren werden nach Heidelberg die Größen in Mathematik und Informatik eingeladen, organisiert von Klaus-Tschira-Stiftung und dem Heidelberg Institute for Theoretical Studies. Die Veranstaltung ist eine Kopie des Nobelpreisträgertreffens in Lindau, nur ohne Nobelpreisträger, denn die gibt es bekanntlich nicht in Mathematik und Informatik. Also werden statt dessen die Träger des Turing-Awards der Association for Computing Machinery sowie des Nevanlinna-Preises und der Fields-Medaille der IMU eingeladen, sowie des Abelpreises der Norwegischen Akademie der Wissenschaften. Auf den Weg gemacht haben sich dieses Jahr 26 Laureaten.
Die Idee der Veranstaltung: 200 junge Wissenschaftlerinnen und Wissenschaftler aus aller Welt treffen sich fünf Tage lang mit den alten Hasen in ihrem Fach, plaudern und halten Vorträge und Workshops. Hier ein paar Impressionen vom Auftakt:
Shigefumi Mori (Fields-Medaille 1990) in Doppelfunktion, hier als amtierender Präsident der IMU.
Ein Erinnerungsfoto!
Leslie Lamport (Turing Award 2013) im Gespräch mit Leonard Adleman (Turing Award 2002)
Empfang im Heidelberger Marstall
Urgestein John Tate (Abel-Preis 2010) schnackt mit einer Musikerin
Das HLF entpuppt sich als eine Mischung aus wissenschaftlicher Tagung und Mensa-Treffen - eine Art Socializing von gutgelaunten Hochbegabten. Unter den Laureaten ist übrigens keine Frau. Unter den jungen Wissenschaftlerinnen und Wissenschaftlern kommt eine Mathematikerin auf etwa 2,6 Mathematiker und eine Informatikerin auf etwa 2,0 Informatiker. Anders ausgedrückt: Die Zutaten zum HLF sind auf der Zuhörerseite 37% Mathematiker, 32% Informatiker, 16% Informatikerinnen, 14% Mathematikerinnen (alles ungefähr, daher die Summe 99%).
Den lockeren Charakter der Tagung (siehe Post davor) förderte übrigens ein Talk von Manuel Blum. Blum wird älter, und so beschäftigte sich sein Vortrag (so wie der des letzten Jahres schon) mit einem Verfahren, Passwörter für Webseiten zu generieren. Blums Vorschlag: Man entwickelt ein "Scheme", eine Funktion, die ein geheimes Passwort (das für alle Webseiten dasselbe ist) und den Namen der Webseite, etwa EBAY, in ein Passwort für die Seite transformiert. Mit dem Trick braucht man sich nur das Scheme und ein einziges Passwort zu merken.
Blum demonstrierte mit Freiwilligen auf der Bühne, das die Sache (wenig überraschend) funktioniert. Und er verriet ein mögliches Scheme: Man ordnet eine Teilmenge einer Permutation des Alphabets (und eventuell auch Zahlen) - also das Passwort - in einer Matrix an und transformiert damit den Namen der Webseite folgendermaßen: Der erste Buchstabe wird auf seinen Nachbarn in der Matrix eine Zeile höher, der zweite Buchstabe auf den Nachbarn rechts, der dritte Buchstabe auf den Nachbarn in der Zeile darunter und so weiter abgebildet. Als Hausaufgabe gab Blum seinen Zuhörern folgende Liste mit:
Aufgabe: Finde das Scheme!
Übrigens: Wenn ein Buchstabe nicht in der Matrix zu finden ist, etwa, weil er nicht im Passwort vorkam, dann entsteht eine Lücke im Code, die man entweder ignorieren kann oder auch durch ein $ füllen könnte. Man darf bei der Definition seines Schemes nämlich durchaus kreativ sein - man muss sich nur merken, wie es funktionierte. Sonst bleibt wieder nichts anderes als ein Klick auf den Knopf "Passwort vergessen?"
Manuel Blums Vortrag enthielt übrigens kein handfestes Resultat. Ganz anders der Talk von Leonore Blum, seiner Gattin. Die hielt nämlich wenig später einen Vortrag über Turings wenig bekannte Arbeiten von 1947, in denen er die LU-Zerlegung von Matrizen beschreibt - verwandt mit der Cholesky-Zerlegung von Matrizen - und untersuchte, wie man messen kann, wie "gut" im numerischen Sinne ein lineares Gleichungssystem gestellt ist. Die Spuren dieses Konzepts der "Konditionierungszahl" verfolgte Leonore Blum bis in die Gegenwart, bis zu modernen Arbeiten aus der Numerik, etwa denen von James Milton Renegar, Jr. und der Smoothed Analysis, für die Dan Spielman 2010 den Nevanlinna-Preis bekommen hat.
Leonard Adleman ist das A in RSA, dem Verschlüsselungsalgorithmus schlechthin. Er ist Turing-Preisträger von 2002. Er boxt in seiner Freizeit (nur ein bisschen, und nicht mehr mit echten Gegnern). Und er befasst sich seit Jahrzehnten damit, wie man mit DNA rechnen kann.
Auf dem HLF verriet er, dass in seinem Portemonaie, da, wo andere die Fotos ihrer Kinder haben, die Kopie des Covers eines nature-Heftes vom März 2006 steckt: In Nature 440, S. 297-302 nämlich veröffentlichte Adlemans Doktorsohn Paul W. K. Rothemund seinen Artikel "Folding DNA to create nanoscale shapes and patterns", in dem er beschreibt, wie er DNA dazu gebracht hat, Smileys und andere Formen zu bilden. Worauf Adleman wahnsinnig stolz ist.
Mit der Bio-Informatik war Adleman ziemlich früh dran; heute muss jeder Informatiker, der etwas auf sich hält, irgendwas mit den Leuten aus dem Biologie-Institut nebenan am Laufen haben. Adleman selbst träumt davon, dass in einigen Jahrzehnten Computer so etwas wie eine eigene Spezies sein sollen, die den Menschen dienen. Aber: Die Mathematik scheint ihm doch zu fehlen. "Ich sage nicht selten zu Mathematikern, rechnet nicht so viel. Und, hey, ich bin der Informatiker." Glaubt man kaum, angesichts der Forschung, die Adleman in den letzten zehn Jahren neben der Bio-Informatik getrieben haben will: Riemann-Flächen und "auch ein bisschen hyperelliptische Kurven und Zahlentheorie". Vielleicht hat er da einen neuen Trend entdeckt?
Eine neue Verschlüsselungsmethode ist Adleman übrigens bei aller mathematischen Arbeit noch nicht eingefallen. Erstmal.
Nun kam Vladimir Voedvodsky, alle hatten auf ihn gewartet.
Sein Mathematikstudium an der Lomonossow-Universität Moskau brach er vor dem formalen Abschluss ab; seine Studienleistungen wurden ihm später als Bachelor anerkannt. Stattdessen beschäftigte er sich selbständig und intensiv mit algebraischer Geometrie; um zu lernen, suchte er den direkten Kontakt zu Wissenschaftlern, allen voran mit Jurij Schabat und später Michail Kapranov. Letzterer verhalf ihm später zu einer Doktorandenstelle in Harvard, wo er 1992 über „Homology of Schemes and Covariant Motives" promovierte. 2002 bekam er die Fields-Medaille, vor allem für seine allgemeine Homotopie-Theorie für algebraische Varietäten und seinen Beweis der Milnor-Vermutung.
Seit diesen Jahren beschäftigt er sich mit der Verifizierung von Beweisen in der reinen Mathematik per Computer. 2010 rief er das "Univalent Foundations Program" offiziell aus, dem jetzt ein Software-Paket entsprungen ist: "UniMath", eine Library für Coq, einen Beweis-Assistenten. Damit lassen sich Beweise formalisieren und per Software die logischen Schlüsse checken, wahlweise mit dem Axiom vom ausgeschlossenen Dritten oder ohne.
"Ich will das Alltagsleben in der Mathematik einfacher machen", sagte Voevodsky auf der Tagung, und träumte davon, dass man mit UniMath seine Beweise in formalisierter Form der Journal-Version zur Seite stellen könnte. "Heute legen viele zu großes Gewicht auf die Ideen statt auf Beweise."
Er selbst geht seit einiger Zeit mit dem guten Beispiel voran: Er arbeite seit einiger Zeit in seinen Arbeiten im Arxiv jeden kleinen Beweis aus, verspricht er. "Ich unterdrücke die Stimmen in meinem Kopf, die sagen, das ist doch trivial. Das sieht doch jeder. Und am Ende ist das Ausarbeiten dann sehr befriedigend."
Die Teilnehmer ließ der Vortrag indessen etwas ratlos zurück: "Was ist das große Ziel?" war die am häufigsten gestellte Frage. Und so richtig klar wurde auch nicht, was UniMath nun genau ausmacht. Der Meister empfiehlt, die Readme-Datei auf github zu lesen - doch auch aus der wird man nicht recht schlau...
Voevodsky zum Zweiten: Heute die "Pressekonferenz" in kleiner Runde, die schnell zum mitunter sehr persönlichen Gespräch mit einem großen Menschen wurde. Natürlich hatte sich Voevodsky viel mehr mit "UniMath" gedacht, als in seinem Vortrag im Publikum angekommen war.
Wie sieht nun der Zeitplan für UniMath und das formale Beweisen im Allgemeinen aus? Die ersten Milestones seien schon geschafft, stellt Voevodsky zufrieden fest: Die Formalisierung des Beweises der Kepler-Vermutung im Projekt "Flyspek" und des Vierfarbensatzes. "Für mich wäre ein wichtiger Meilenstein, wenn ein experimenteller Kurs in abstrakter Algebra mit Hilfe unseres Beweissystems gehalten würde." Das Lehrbuch dazu zu schreiben hat Voevodsky nicht vor, da sollen andere ran. "Im Moment arbeite ich daran, zu zeigen, dass, was in UniMath bewiesen ist, ein klassischer Beweis ist, in folgendem Sinne: Wenn etwas in UniMath bewiesen ist, dann gibt es eine Garantie dafür, dass es in einen formalen Beweis in Zermelo-Fraenkels Theorie übersetzt werden kann. Das ist, wovon meine Paper derzeit handeln."
Doch etwas ganz anders könnte zum richtig großen Meilenstein für UniMath werden - oder zum PR-Desaster: Ein formaler Beweis der ABC-Vermutung, die der Japaner Shin’ichi Mochizuki angeblich bereits bewiesen hat (nur hat niemand außer ihm bisher seinen Beweis voll durchgearbeitet, geschweige denn verstanden). Ein solches Projekt zu formalisieren ist alles andere als einfach und birgt viele Risiken. Und was, wenn sich schließlich der Beweis als falsch herausstellt und das auf UniMath zurückfällt? Entsprechend vorsichtig äußert sich Voevodski: "Ich bin sehr neugierig darauf, was die Wahrheit ist." Loslegen müsste wieder jemand anderer als er - und hoffentlich zum Ziel kommen.
Auf jeden Fall kann aber in der Zwischenzeit schon mal jedermann vom Beweisen mit Computern profitieren, in der täglichen Arbeit: "Für mich ist einer der Vorteile, das er den Geist diszipliniert. Er bringt mich mehr zu den Wurzeln dessen, was einen Beweis eigentlich ausmacht. In Mathematik gibt es diese Krankheit, sich zu schämen, in seinen Beweisen zu elementar zu sein. Diese Krankheit ist ansteckend, auch über Generationen hinweg und schlecht für die Mathematik. Und einer der Effekte des Beweisassistenzen war, dass ich von dieser Krankheit praktisch geheilt bin. Das spiegelt sich jetzt in meinen Papern wider."
Ich habe mir jedenfalls jetzt mal Coq heruntergeladen und installiert. Als ersten Schritt.
Interview mit Sir Michael Atiyah - und wir kommen hinterher aus dem Zimmer mit einer Liste guter und poetischer Ratschläge.
Kollaborationen: "Du lernst von deinen Ko-Autoren. Du weitest dein Wissen. Mathematik kann eine einsame Angelegenheit sein. Für deine eigene Gesundheit kann es gut sein, zusammenzuarbeiten. Du redest, du genießt dein Leben, du trinkst dein Bier, du verbringst Ferien zusammen. Und das integriert die Arbeit in dein Leben. Und das verschafft dir ein normaleres, fröhlicheres Leben."
Computeruntersützung: "Da kommt vermutlich gute Arbeit zweiter Klasse heraus. Wir verlieren die Individualität. Wenn du zu formal wirst, tötest du die Träume."
Preise: "Du solltest dich um deine Arbeit kümmern. Wenn du einen Preis bekommst, dann ist das zweitrangig."
Fragen: "If you ask the simpler questions, you get the deeper answers."
Einen schönen Vortrag habe ich noch unterschlagen: Den von Endre Szemerédi, einem Kombinatoriker, der 2012 den Abelpreis erhalten hat.
Es ging um eine Variation über ein Thema aus Szemerédis Lebenswerk: arithmetische Progressionen, also Folgen der Form a, a+k, a+2k, a+3k,..., und zwar in Teilmengen der Menge der natürlichen Zahlen von 1 bis N.
Szemérdi erklärte die Methode für seinen Beweis von 1980 (den er erst 2007 veröffentlichte), der besagt, dass
r3(N) ⩽ N / ( e(1/100) * sqrt(log(log(N))) )
ist, dass also Mengen, die mehr als so viele Elemente enthalten, sicher auch eine arithmetische Progression der Länge 3 enthalten, also drei Zahlen a, a+k und a+2k für irgendein k. Zum Vergleich: Die aktuell beste Schranke beträgt
r3(N) ⩽ N log(log(N))4 / log(N).
(Wer jetzt übrigens eine Assoziation zu einem berühmten Paper von Ben Green hat, der liegt liegt nicht ganz verkehrt: Ben Green hat bewiesen, dass in den Primzahlen unendlich viele arithmetische Progressionen der Länge 3 vorkommen. Nur -- hier geht es nicht um Primzahlen.)
Der Traum der Zahlentheoretiker wäre ein Beweis dafür, dass auch die Schranke
r3(N) ⩽ N / log(N)k
gilt. Und diese Schranke kann man übersetzen, in die Sprache der Graphentheorie: Man betrachtet einen Hypergraph auf N Knoten, in dem alle Hyperkanten genau drei Knoten verbinden und in dem keine Teilmenge von sechs Knoten drei Hyperkanten enthält. Wenn man zeigen könnte, dass die Anzahl der Kanten dann kleiner oder gleich
c N2/log(N)k
ist, für jedes beliebige c größer Null -- also "small oh" von N2/log(N)k --, dann hätte man auch die Traumschranke von oben gezeigt.
Andreas Loos