Die Digitalisierung der Mathematik

Eine 100 Jahre alte Utopie wird wiederbelebt: die Digitalisierung der Mathematik durch formale Beweise. Ein Gastbeitrag von Dr. Sebastian Schleißinger (Mathematiker).

Wenn Kevin Buzzard über die Zukunft der Mathematik vorträgt, dann löst seine Vision einerseits lebhafte Begeisterung aus, andererseits ebenso große Skepsis. Seine Idee: Hätte man die gesamte bekannte Mathematik formalisiert und in einer digitalen Datenbank gespeichert, dann wäre sie für Algorithmen überprüfbar und alle Fehler, alle Beweislücken, die sich in der großen Zahl an Publikationen versteckt halten, würden schließlich aufgedeckt werden. Eine neue, ultimative Qualität mathematischer Exaktheit. Die Unterstützer dieser Vision sehen darin gar die Schritte in eine neue Ära mathematischer Forschung, in der künstliche Intelligenz (KI) auf Basis dieser Datenbank trainiert wird, Mathematik selbständig erlernt und uns Menschen schließlich in ihrer Erforschung übertrifft. Die Kritiker halten dagegen: alles nichts Neues und schon seit 100 Jahren maßlos überschätzt.

Buzzard, Professor für Mathematik am Imperial College London, geht jedenfalls selbst mit gutem Beispiel voran und hat sein erstes Etappenziel fest im Blick: Zunächst soll der komplette Lehrplan des Bachelor-Studiums Mathematik an seiner Universität formalisiert werden. Er verwendet hierfür die formale Sprache Lean. „Formalisieren“ bezieht sich hierbei nicht etwa auf das übliche Digitalisieren von Literatur, sondern auf das Übersetzen mathematischer Resultate, und vor allem deren Beweise, in eine ungleich detailliertere Sprache, die keinen noch so kleinen Argumentationsschritt auslässt und somit von Computern verstanden werden kann.

Um die aktuell bekannte Mathematik zu formalisieren, wäre eine gewaltige Übersetzungsarbeit notwendig. Umso bewundernswerter sind Teams, die sich systematisch dem Formalisieren einzelner Teilbereiche widmen, oftmals bestehend aus Studierenden. So bietet Buzzard Seminare und Vorlesungen zu Lean an, in denen er formales Beweisen unterrichtet und seine Studierenden zugleich zum Mitmachen einlädt. Hinzu kommen Vorträge an anderen Instituten, um auch insbesondere Informatiker dafür zu begeistern, welche erfahrungsgemäß offener für neue digitale Utopien sind. Lean wurde 2013 von Leonardo de Moura als frei zugängliches Projekt ins Leben gerufen und seitdem wächst die Lean-Bibliothek kontinuierlich an. Auch Promovierende und Post-Docs der Mathematik machen bereits mit und bauen auf den schon vorhandenen Grundlagen auf, mit dem Ziel, beim Formalisieren möglichst weit in ihren eigenen Forschungsbereich vorzustoßen. Für diese Arbeit braucht es neben Motivation vor allem Zeit und so ist es nicht verwunderlich, dass während der Corona-Pandemie die Anzahl an formalisierten Aussagen in Lean beachtlich angestiegen ist [1]. Buzzard wurde selbst inspiriert durch den Mathematiker Thomas Hales, welcher seinen eigenen Beweis der Kepler-Vermutung nach jahrelanger Arbeit formalisiert hatte und nach diesen Erfahrungen mit Ideen einer digitalen Zukunft der Mathematik spielte. Würden alle mathematische Objekte digitalisiert werden, so könnten sie in einer Art „Google Earth für Mathematik“ erkundet werden und das, was aktuell unüberschaubar ist, würde vernetzt und leichter zugänglich sein [2]. Doch ist das Digitalisieren von Mathematik in diesem Sinne überhaupt möglich? Können Glanzleistungen menschlicher Geisteskraft wie der Satz des Pythagoras, Differentialgeometrie, Relativitätstheorie, etc., prinzipiell in Computern abgebildet werden?

Was ist ein Beweis?

Ironischerweise führt diese Frage direkt zu den Anfängen der Digitalisierung selbst. Die theoretische Beschreibung von Computern (durch Alan Turing, Alanzo Church, John von Neumann, etc.) fällt zeitlich mit der sogenannten Grundlagenkrise der Mathematik zusammen. Im 19. Jahrhundert hatte sich die Mathematik im Vergleich zu ihren antiken Vorbildern, wie der Geometrie von Euklid und den Zahlen von Pythagoras, erheblich weiterentwickelt. Dies führte nun zu der Frage, ob denn wirklich alle Mathematiker auf die gleiche Weise Mathematik betrieben? Wenn von mathematischen Objekten wie der Menge der natürlichen Zahlen gesprochen wurde, meinten dann alle dasselbe, oder wurden hier und da Äpfel mit Birnen verglichen? Und noch schlimmer: Waren sich wirklich alle einig, wann ein Beweis als Beweis zählte?

Ein Beweis einer Aussage wurde gemeinhin als Folge logischer Argumentationsschritte verstanden, die aus Axiomen, d.h. Aussagen, die ohne Argument einfach als wahr angenommen werden, jene Aussage herleiten. Völlig unklar war allerdings, ob überhaupt Einigkeit über die verwendeten Axiome sowie der zu Grunde liegenden Beweislogik bestand. Zu Beginn des 20. Jahrhunderts wünschte sich die Mathematik-Welt ein neues logisches Fundament. Als Kandidat wurde schnell die Mengenlehre gefunden. Doch nun kam die Frage auf, wie ein Axiomensystem der Mengenlehre aussehen müsste, aus dem sich alle Mathematik logisch korrekt und ohne Widersprüche folgern ließe. Diese Probleme wurden zu Beginn des 20. Jahrhunderts von Größen wie David Hilbert, Bertrand Russell und dem genialen Logiker Kurt Gödel bearbeitet. Ein Erfolg schien zum Greifen nahe, als Russell zusammen mit Alfred North Whitehead ein Axiomensystem einer sogenannten Typentheorie erstellt hatte. In ihrem Werk „Principia Mathematica“ hatten sie begonnen, hieraus in der notwendig pedantischen Kleinstarbeit fundamentale mathematische Aussagen abzuleiten. Erst nach mehr als 700 Seiten wird die Aussage 1+1=2 bewiesen. Mathematiker hätten nun diese auf Papier begonnene Datenbank des mathematischen Wissens weiter füllen können, doch dann kam Kurt Gödel. Gödel hat mit seinem Unvollständigkeitssatz gezeigt, dass weder das Russellsche noch irgendein anderes Axiomensystem die gewünschten Kriterien prinzipiell erfüllen kann, ein Todesstoß für das gewünschte axiomatisierte Fundament der Mathematik. Gödel konnte mathematisch beweisen, dass es solch ein Axiomensystem gar nicht geben kann, denn entweder würde es Widersprüche wie 1=2 zulassen, damit wäre es schlichtweg unsinnig, oder es wäre unvollständig, so dass sich Aussagen formulieren ließen, die weder bewiesen noch widerlegt werden könnten. Gödels Satz stellt schwer verdauliche mathematische Erkenntnis in die Grenzen der Erkenntnis selbst dar, was bis heute vor allem in der Philosophie diskutiert wird.

Unter dem Eindruck dieses philosophischen Schocks wird leicht vergessen, dass der große Teil der bekannten Mathematik von dieser Einsicht gänzlich unberührt blieb und dass die Grundlagenkrise durchaus befriedigend gelöst wurde. Der überwiegend große Teil der damaligen und auch der heutigen Mathematik wurde in der Tat auf ein einheitliches Gerüst gestellt, üblicherweise die Mengenlehre, die durch das ZFC-Axiomensystem beschrieben wird (ein Axiomensystem, das von Ernst Zermelo und Abraham Fraenkel aufgestellt wurde und um das Auswahlaxiom, „axiom of choice“, ergänzt wird); alternativ kann auch eine zu den ZFC-Axiomen äquivalente Typentheorie verwendet werden. Sind diese Axiome widerspruchsfrei, so impliziert der Unvollständigkeitssatz, dass es zwar Aussagen über diese Mengenlehre gibt, die weder bewiesen noch widerlegt werden können (davon sogar unendlich viele), doch spielen diese Aussagen in der Praxis so gut wie keine Rolle und sind vielmehr sporadische Ausnahmen. Diese Ausnahmen können dann gesondert in anderen Axiomensystemen studiert werden. Stehen die Beweislogik und das Axiomensystem fest, so ist das Beweisen von Aussagen nichts anderes als das Manipulieren von Zeichenketten nach gewissen Regeln. Formal gesehen ist Mathematik damit mit Spielen wie Schach vergleichbar: eine Zugfolge nach festen Regeln angewandt auf eine Ausgangsposition, den Axiomen. Beispielsweise stellen die zu Grunde liegenden Axiome in Lean eine zu den ZFC-Axiomen äquivalente Typentheorie dar. Eine offene Vermutung stellt also die Frage nach einer Zugfolge, die aus den Axiomen jene neue Aussage herleiten kann. Historisch gesehen erhielt ein Beweis somit seine Gültigkeit durch seine Übersetzbarkeit in einen von Computern überprüfbaren formalen Beweis.

Keine Macht den Fehlern

Das Publizieren mathematischer und naturwissenschaftlicher Arbeit geschieht meist im Peer-Review-Verfahren, d.h. ein neues Werk wird bei einem Fachjournal eingereicht und ein oder mehrere Experten aus dem entsprechenden Fachgebiet bewerten die Arbeit nach ihrer Korrektheit, Signifikanz, Neuheit, usw. Dieses Verfahren hat sich im Laufe der Zeit bewährt, insbesondere in der Mathematik. Gleichzeitig ist dieses System nicht frei von Mängeln, zumal es völlig neutrale, gewissenhafte und objektive Gutachter voraussetzt.

In mathematischen Publikationen werden Leser nicht selten dazu aufgefordert, sich um ausgelassene Details selbst zu kümmern, etwa bei kleineren Rechnungen oder gängigen Standardargumenten. Stillschweigend wird dabei vorausgesetzt, dass diese Details auch wirklich nur Details sind und von den Gutachtern sorgfältig geprüft wurden. Schon rein statistisch betrachtet wird dies nicht immer der Fall sein und folglich muss es innerhalb der gesamten publizierten Mathematik eine gewisse Zahl an Beweislücken sowie an fehlerhaften Beweisen und Theoremen geben. Dies ist dann umso schlimmer, wenn die entsprechenden Resultate wiederum in anderen Arbeiten zitiert und weiterverarbeitet werden. Glücklicherweise führt der wiederholte Gebrauch eines falschen Satzes oftmals zur Entdeckung des Fehlers, wenn sich nämlich plötzlich ein Widerspruch innerhalb einer Theorie ergibt, und so besitzt die mathematische Community eine Art automatischer Fehlerkorrektur. Es ist schwierig abzuschätzen, wie viele fehlerhafte Theoreme insgesamt publiziert sind. Offensichtlich sind immerhin die zunehmenden Anreize für schnelles, oberflächliches Begutachten. Der große Publikationsdruck fördert das flüchtige Überprüfen und Abnicken neuer Arbeiten. Hinzu kommt die Tatsache, dass sich das Begutachten für Fachjournale innerhalb der Mathematik meist als unbezahlte Nebentätigkeit etabliert hat.

Auch die exakteste aller Wissenschaften lässt also noch Raum für mehr Exaktheit. Beim Formalisieren mathematischer Resultate würden zwangsläufig alle Beweislücken geschlossen und jeder noch so kleine Fehler aufgedeckt werden. Kritiker sehen in einer solchen Vorgehensweise eine nutzlose Pedanterie, bei der zudem noch die Schönheit der Mathematik verloren ginge, denn die eleganten Beweisideen würden dann beim Zerteilen in viele kleine Schritte untergehen. Wenn Buzzard seine Kollegen fragt, wie sie reagieren würden, wenn sich beim Formalisieren plötzlich herausstellte, dass eines ihrer Ergebnisse irreparabel falsch wäre, so gibt es bemerkenswerter Weise auch achselzuckende Antworten: Zwar wären die Ideen des Beweises dann falsch, aber noch immer elegant und selbst mit Fehlern von unleugbarer Schönheit – menschlich, allzumenschlich.

Doch interessanterweise kann das Formalisieren auch umgekehrt zu mehr Einsicht verhelfen. Buzzard gelang es, zusammen mit Johan Commelin und Patrick Massot, den von Peter Scholze entwickelten Begriff des „perfektoiden Raumes“ zu formalisieren, eine komplexe Struktur aus der aktuellen Forschung. Scholze wurde 2018 für die Einführung dieses Begriffs und seine Arbeiten auf dem Gebiet der algebraischen Geometrie die Fields-Medaille verliehen, eine der wichtigsten Auszeichnungen für Mathematiker. Buzzard berichtet über seine Formalisierungs-Erfahrungen regelmäßig in seinem Blog [3]. Dort hatte nun Scholze in einem Gastbeitrag im Dezember 2020 dazu aufgerufen, ein schwieriges Theorem aus der Geometrie zu formalisieren, von dem er den Beweis zwar prinzipiell gefunden hätte, allerdings nicht ganz ohne Zweifel bei manchen Details. Die Community nahm die Herausforderung an und sechs Monate später konnte etwa die Hälfte des Beweises formalisiert werden, was Scholze bereits tatsächlich weiterhalf. Sein Fazit: „Ich habe gelernt, dass es jetzt möglich ist, eine Forschungsarbeit zu nehmen und einem Beweis-Assistenten ein Lemma nach dem anderen zu erklären, bis alles formalisiert ist! Ich denke, das ist eine bahnbrechende Leistung.“ [4]

Computer und Beweise

Mathematische Sätze beziehen sich meist auf eine unendlich große Grundgesamtheit gewisser mathematischer Objekte. Hin und wieder beweisen Mathematiker, dass eine Vermutung bis auf endlich viele Fälle richtig ist. Ist die Anzahl N dieser Ausnahmefälle nun hinreichend klein, so lassen sie sich einfach per Hand überprüfen. Geht N allerdings in die Tausende und Millionen, so bietet sich eine Überprüfung durch einen Computer an. Hat dieser nach stundenlanger Rechenzeit alle Fälle positiv beantwortet, so stellt sich die Frage, wie ein Begutachten dieser Rechenarbeit möglich sein kann. Die Gutachter könnten zwar den Programmcode überprüfen - zumindest den von Menschen verfassten Teil - und die Berechnung mit dem eigenen Computer wiederholen. Doch dies führt meist zu praktischen als auch theoretischen Schwierigkeiten. Aus praktischer Sicht müssen sich die Experten nicht nur im entsprechenden Fachgebiet auskennen, sondern zudem den verwendeten Algorithmus nachvollziehen, sich mit der jeweiligen Programmiersprache auskennen und schließlich die Korrektheit des Programmcodes verifizieren. Eine Arbeit, die gerne mehrere Jahre in Anspruch nehmen kann. Aus theoretischer Sicht stellen sich noch weitere Fragen, z.B. ob der Code von einem korrekten, unmanipulierten Compiler übersetzt wurde? Noch allgemeiner: Funktioniert jegliche Soft- und Hardware korrekt, die beim Überprüfen des Beweises involviert ist?

Als Paradebeispiel für diese Problematik dient die Kepler-Vermutung, eine Hypothese von Johannes Kepler über die dichtesten Kugelpackungen im dreidimensionalen Raum. 1998 reichte Thomas Hales einen Beweis dieser Vermutung beim renommierten Fachjournal Annals of Mathematics ein. Der Beweis enthielt allerdings 3 Gigabyte an Computerberechnungen. Erst fünf Jahre später akzeptierten die Gutachter den Beweis mit dem Hinweis, sie seien sich dessen Richtigkeit zu 99% sicher. Inwiefern sollte die Vermutung nun als gelöst betrachtet werden?

Einfacher handzuhaben wären solche Fälle, wenn Beweise in einer allgemein akzeptierten formalen Sprache verfasst wären. Ähnlich zum Textsatzsystem TeX, welches in Mathematik und Informatik nahezu ausnahmslos genutzt wird, würden Mathematiker eine weitere, eine formale Sprache in ihren Werkzeugkasten hinzufügen, mit dem sie Probleme jener Art bewältigen könnten. Aus praktischer Sicht würde das Verifizieren eines Computerbeweises von der Informatik weg und wieder näher zur Mathematik gebracht werden. Auch die theoretischen Einwände würden so entkräftet, z.B. liefert Lean einen formalen Beweis für die Korrektheit des Compilers (geschrieben in Lean) gleich mit. Dieses formale Verifizieren lässt sich auf jegliche Soft- und Hardware ausdehnen. Tatsächlich hat sich die Verwendung formaler Beweise gerade am anderen Ende der Kette bereits etabliert. Computer-Chips werden mittlerweile mit zuverlässigeren, formalen Methoden verifiziert, statt sie stichprobenartigen Tests zu unterziehen.

Um den Restzweifel an seinem Beweis zu beseitigen, rief Hales 2003 das Projekt „Flyspeck“ ins Leben, dessen Ziel eine vollständige Formalisierung des Beweises war. Dieses Projekt wurde 2015 erfolgreich abgeschlossen und das Maximum an Vertrauen in den Beweis wurde erreicht.

Klar, ein Restzweifel bleibt beim Einsatz von Computern stets bestehen und an irgendeiner Stelle muss der Mensch der Maschine ganz einfach Vertrauen schenken. Doch Skeptiker mögen sich umgekehrt die Frage stellen, wie „korrekt“ das Gehirn eines Gutachters arbeitet. Beim Lesen eines Minuszeichens, das über Auge und Sehnerv geleitet und im Gehirn als sensorischer Impuls interpretiert wird, könnte am Ende nur allzu leicht ein Pluszeichen stehen. Ein einziger Vorzeichenfehler reicht allerdings schon, um im Pfad eines mathematischen Arguments falsch abzubiegen.

Der Einsatz von Computern bei Beweisen wird ständig weiterentwickelt, z.B. von Informatikern wie Marijn Heule, ein Experte für Computerbeweise. Ihm ist es schon mehrfach gelungen, ungelöste mathematische Probleme so umzuformulieren, dass sie von Computern in Angriff genommen werden können. Erfolg hatte seine Methode bei der endgültigen Lösung der Keller-Vermutung, sowie bei einem Problem über Pythagoräische Zahlentripel. Bei letzterem wurde die Rechenarbeit dem Supercomputer Stampede der University of Texas at Austin überlassen, welcher nach zwei Tagen 200 Terabyte an Rechnungen ausspuckte. Doch es geht noch größer: Wieder mit Hilfe eines Supercomputers hat Heule die „fünfte Schur-Zahl“ berechnet, Ergebnis: 160, Beweisgröße: 2000 Terabyte [5]. Heule hat sich auch am hartnäckigen Collatz-Problem versucht, bisher erfolglos, doch die Fachwelt schaut gespannt auf Fortschritte, die Forscher wie Heule beim Einsatz von Computern erzielen.

Digitalisierung von Mathematik

Das Digitalisieren von Mathematik mittels formaler Beweise würde ein höheres, kaum zu überbietendes Vertrauen in die Korrektheit mathematischer Argumentationen bringen. Stellt man sich eine Datenbank vor, in der die gesamte bekannte Mathematik formalisiert wäre, so wären vermutlich schon die üblichen Funktionen „suchen, filtern, sortieren“ neue mächtige Werkzeuge. Ob wir Menschen dann von KI-Algorithmen profitieren würden, die eine solche Datenbank selbständig erweitern, steht in den Sternen. In der Geschichte gab es bereits Beispiele für beides: das Überschätzen künstlicher als auch menschlicher Intelligenz, und noch fehlen einfach die Daten, mit denen maschinelles Lernen trainiert werden könnte.

Zum mathematischen Alltag gehört immerhin noch mehr als das Beweisen: interessante Vermutungen aufstellen, exotische Beispiele finden, der intra- und interdisziplinäre Austausch über neue Fragestellungen, usw. Doch umgekehrt zeigen die Arbeiten von Forschern wie Buzzard, Hales und Heule, dass das Formalisieren komplexer Mathematik aus der aktuellen Forschung nicht nur möglich ist, sondern sogar zum Verständnis beitragen kann und Computer beim Lösen schwieriger mathematischer Probleme helfen können. In diesen Fällen spielen Computer nicht die Rolle eigenständiger KI, sondern sind vielmehr als erweiterte Intelligenz, „augmented intelligence“, des Menschen zu verstehen.

Geradezu unverzichtbar wird formalisierte Mathematik dann, wenn Computer selbst bei Beweisen beteiligt sind. Dies erinnert an die Software-Entwicklung, bei der Programm-Code meist ohnehin nur durch Computer überprüft werden kann. Üblicherweise geschieht dies durch Tests, d.h. durch stichprobenartige Durchläufe des Programms, bei dem der reale mit dem erwarteten Output verglichen wird. Ein größeres Vertrauen aber garantieren formale Beweise, welche eine Art Gütesiegel für die Korrektheit der gesamten Software oder zumindest gewisser Teil-Funktionalitäten ausstellen. Dieses mathematische Verifizieren hat sich bereits in der Industrie für Computer-Chips etabliert und könnte in Zukunft eine größere Rolle spielen. Je größer der Einsatz von Algorithmen, desto größer ist das Verlangen nach Vertrauen in Software.

Aus einer abstrakten Sicht sind Programmieren und formales Beweisen ein und dasselbe. So gesehen wären die für Menschen geschriebenen mathematischen Forschungsarbeiten lediglich Dokumentationen von (noch zu schreibendem) Code. Aus dieser formalistischen Sicht ein fast erschreckender Zustand! Unabhängig von den verschiedenen Sichtweisen lässt sich sagen: Es lohnt sich, Digitalisierung auch als Entwicklung einer erweiterten Intelligenz im Wechselspiel zwischen Mensch und Maschine (nicht nur in der Mathematik) genau zu beobachten. In der Mathematik sind Beweise entweder richtig oder falsch. Die praktische Informatik geht weiter: Es gibt guten und schlechten Code, es gibt den schlampigen Pfusch sowie den exzellenten, mit Bedacht und Struktur entwickelten Code. Seien wir beim Digitalisieren also selbst exzellent!

QUELLEN:

1. https://leanprover-community.github.io/mathlib_stats.html.
2. https://formalabstracts.github.io.
3. https://xenaproject.wordpress.com.
4. https://xenaproject.wordpress.com/2021/06/05/half-a-year-of-the-liquid-tensor-experiment-amazing-developments.
5. M. Heule, Schur Number Five, Proceedings of the AAAI Conference on Artificial Intelligence, 32(1), 2018.
6. G. Gonthier, Formal Proof: The Four-Color Theorem, Notices AMS, 2008.
7. T. Hales: A proof of the Kepler conjecture, Annals of Mathematics, 2005.
8. T. Hales, M. Adams, G. Bauer, T. D. Dang, J. Harrison: A formal proof of the Kepler conjecture. In: Forum of Mathematics, Pi. Band 5, 2017.
9. J. Brakensiek, M. Heule, J. Mackey, D. Narváez, The Resolution of Keller's Conjecture, in: Peltier N., Sofronie-Stokkermans V. (eds) Automated Reasoning, IJCAR 2020, Lecture Notes in Computer Science, vol 12166. Springer, 2020.
10. M. Heule, O. Kullmann, V. Marek, Solving and Verifying the Boolean Pythagorean Triples Problem via Cube-and-Conquer, in: Theory and Applications of Satisfiability Testing - SAT 2016, Springer, 2016.
11. K. Gödel, Über die Länge von Beweisen, Ergebnisse eines Mathematischen Kolloquiums, 1936.
12. https://leanprover-community.github.io, https://leanprover.github.io.
13. K. Buzzard, „The Future of Mathematics“, 05.09.2019, Microsoft Research, Video, Vortragsfolien.
14. https://www.ma.imperial.ac.uk/~buzzard.

Bildnachweise

• Kurt Gödel: https://de.wikipedia.org/wiki/Kurt_Goedel.
• Kevin Buzzard: https://de.wikipedia.org/wiki/Kevin_Buzzard, Lizenz: Paulabuzzard at en.wikipedia (https://commons.wikimedia.org/wiki/File:Kevin_buzzard_in_2007.jpg), „Kevin buzzard in 2007“, https://creativecommons.org/licenses/by-sa/3.0/legalcode.
• Thomas Hales: https://de.wikipedia.org/wiki/Thomas_Hales, Lizenz: Slawekb (https://commons.wikimedia.org/wiki/File:Halescropped.jpg), „Halescropped“, https://creativecommons.org/licenses/by-sa/3.0/legalcode.

Zum Autor:

Dr. Sebastian Schleißinger hat in Würzburg Mathematik studiert und anschließend in komplexer Analysis promoviert. Seine Forschung führte ihn zuletzt zur nichtkommutativen Wahrscheinlichkeitstheorie („quantenstochastische Prozesse“). Trotz seiner Arbeit in Bereichen der „reinen“ Mathematik behielt er sich stets ein offenes Herz für Statistik und Informatik. Er liebt Schokolade und guten Espresso.