Eine Bahnfahrt von Lyon nach Paris ist ein relativ kurzes Vergnügen: Der TGV braucht für die 429 Kilometer gerade mal zwei Stunden – eine knapp bemessene Zeit, wenn man währenddessen seinen Kollegen davon über­zeugen will, seine Arbeit fundamental anders zu machen, als das seit jeher üblich ist.

Der Mathematiker Vladimir Voevodsky hat es trotzdem versucht. Und als kurz vor Paris die Idee seinem Fachkolle­gen Steve Awodey von der Carnegie Mellon University in Pittsburgh (Pennsylvania) immer noch nicht so recht einleuchten will, holt er seinen Laptop aus der Tasche und ruft ein Programm namens Coq auf. Das ist auf den ersten Blick so etwas wie ein spezialisiertes Microsoft Word: Man schreibt in einer hochgradig formalisierten Notation einen mathematischen Text hinein. Im Zug erarbeitet Voevodsky binnen 15 Minuten mit Hilfe eines neuen, von ihm entwor­fenen Formalismus namens "Univalent Foundations" die Definition eines mathematischen Objekts. Eigentlich sei das doch ganz einfach, und Awodey möge doch am besten seine Mathematik nur noch in Coq betreiben.

Voevodsky hat gut reden. Der 48­-Jährige ist permanentes Fakultätsmitglied am weltberühmten Institute for Advanced Study (IAS) in Princeton (New Jersey). In Moskau geboren, spricht er nahezu akzentfreies Englisch und strahlt die Selbstsicherheit eines Menschen aus, der niemandem mehr etwas beweisen muss. Im Jahr 2002 wurde ihm die Fields­ Medaille verliehen, die bedeutendste Auszeichnung auf dem Gebiet der Mathematik. Kaum verwunderlich, wenn er und der Rest der Welt deutlich verschiedene Vorstellungen davon haben, was in der Mathematik einfach ist....