Mathematik auf neuer Grundlage

Bahnt sich in der Mathematik eine regelrechte Revolution an? Eine Umwälzung, welche die Art, wie Mathematikerinnen und Mathematiker arbeiten, grundlegend verändert? Werden in naher Zukunft eher die Computer als die Menschen zuverlässig prüfen, ob ein mathematischer Beweis richtig ist?

Folgt man der Bloggerin Julie Rehmeyer, so hat der russische Mathematiker Wladimir Wojewodski (*1966), Professor des Institute for Advanced Studies in Princeton, tatsächlich einen Ansatz entwickelt, der die Mathematik und ihre Grundlagen revolutionieren könnte: Im Prinzip habe der russische Mathematiker zeigen können, dass die Homotopietheorie, die sich mit der Verformung geometrischer Objekte befasst, dieselben Ideen ausdrückt wie die Theorie der Programmiersprachen und die mathematische Logik, nur in einer anderen Sprache (die Homotopietheorie spielte eine zentrale Rolle in der Arbeit des Russen über die Milnor-Vermutung, für die er 2002 die prestigeträchtige Fields-Medaille erhielt), schreibt sie in einem Blog der populärwissenschaftlichen Zeitschrift «Scientific American».

Wojewodski selbst will zwei Entwicklungsstränge der heutigen Mathematik miteinander vereinigen. Damit er seine Ideen persönlich in Zürich vorstellen kann, hat ihn die ETH im September als Referenten der «Paul Bernays Lectures 2014» eingeladen. Giovanni Felder, der Leiter des ETH-Instituts für Theoretische Studien (ITS) wird seine Forschung dem Publikum an der ETH vorstellen. Er sagt: «Wojewodski entwickelt eine neue Theorie, welche die Mathematik auf ein neues Fundament stellt. Die Fragen, die er dabei aufwirft, betreffen die Grundlagen der Mathematik ebenso wie die der Informatik und der Logik.» Diese Theorie heisst «Homotopie Typen Theorie (HoTT)» und «Univalente Grundlagen der Mathematik» das zugehörige, computerorientierte Projekt.

Eine einfachere Sprache für Computerbeweise

Im Rahmen von «HoTT» entwickelt Wladimir Wojewodski einen Ansatz, mit dem sich mathematische Beweise viel einfacher als heute in eine Programmiersprache von Computer-Beweisassistenten (engl. «proof assistants») übersetzen lassen. Bewährt sich dieser Ansatz, dann könnten Computer in Zukunft auch so komplizierte Beweise prüfen, bei denen selbst profilierten Mathematikern Fehler unterlaufen. «Mithilfe von Computer-Beweisassistenten könnten wir hochkomplexe und hochabstrakte mathematische Theorien bilden», sagt Wojewodski.

Für Mathematikerinnen und Mathematiker wären solche Beweisassistenten keine Nebensache, denn zum einen ist Beweisen so etwas wie ihre Schlüsseltechnik, zum andern erfordern die Beweisassistenten neue Grundlagen der Mathematik. Zum Ersten: Um akzeptiert zu werden, müssen Beweise in der Mathematik korrekt sein und die logischen Regeln einhalten. Ihre Richtigkeit muss sich fehlerlos und aus bestimmten, wahren Grundsätzen (Axiomen) und bereits bewiesenen Aussagen herleiten lassen. Der Traum vieler Mathematiker war und ist es, jene Axiome zu formulieren, aus denen heraus sich möglichst alle mathematischen Sätze widerspruchsfrei herleiten und beweisen lassen.

Mengenlehre ist schwierig zu übersetzen

Ein solches System von Axiomen stellte Ernst Zermelo 1908 vor. Heute ist es als Zermelo-Fraenkel-Axiomatik der Mengenlehre bekannt und dient auch als Fundament der gesamten Mathematik, da sich alle mathematischen Objekte auch als Mengen interpretieren lassen.

Der Nachteil der Mengenlehre ist, dass ihre Grundsätze nur sehr schwierig in die Programmiersprache eines Beweisassistenten zu übersetzen sind. Die heute bestehenden Beweisprogramme, wie etwa das «coq», das Wojewodski verwendet, beruhen denn auch auf der Typentheorie , die der englische Mathematiker und Philosoph Bertrand Russell (1872-1970) als Alternative zur Mengenlehre vorgeschlagen hat.

Innovativ an Wojewodskis Ansatz ist, dass er die Aussagen des formalen Systems der Typentheorie in der Sprache der Homotopietheorie interpretiert. In dieser Interpretation gilt dann eine zusätzliche Eigenschaft, die sogenannte Univalenz, die Wojewodski als neues Axiom zu den Grundlagen der Mathematik hinzufügt. Darin setzt er die Gleichheit logisch-mathematischer Aussagen in Beziehung zur Gleichwertigkeit im Sinne der Homotopietheorie.

Tasse und Donut: Eine reichhaltigere Sprache

Dieser Ansatz mag zunächst erstaunen, denn eigentlich befasst sich die Homotopietheorie damit, wie man verschiedene geometrische Objekte durch Verformungen ineinander überführen kann. Anschaulich zeigen lässt sich das an einer Tasse und einem Donut: Mit Blick auf ihre Form sehen beide völlig verschieden aus. Mit Blick auf ihre Eigenschaften sind sie jedoch beide ein «Objekt mit einer Öffnung». Der Donut ist ein Ring und die Tasse hat einen Henkel. Zudem lässt sich die Tasse so in einen Donut umwandeln, dass Punkte, die auf der Tasse nebeneinander liegen, auch auf dem Donut benachbart sind. Die zwei intuitiv verschiedenen Objekte haben somit gleiche Eigenschaften. Sie sind äquivalent oder gleichwertig, wie die Mathematiker sagen.

Dieses Äquivalenz-Problem stellt sich auch bei der Interpretation von Gleichungen, die in der Mathematik und in Programmiersprachen verwendet werden. Eine Gleichung wie «a=b» ist eine mathematische Aussage, bei der zwei verschiedene Symbole denselben Wert haben. Das entspricht logisch den zwei unterschiedlichen Formen mit strukturell gleichen Eigenschaften.

Gleiche Idee, verschiedene Sprachen

«Durch Wojewodski wissen wir nun, dass man solche Gleichheitsbeziehungen in der Homotopietheorie besser formulieren kann, weil sie eine reichhaltigere Theorie ist», sagt Giovanni Felder. Die Homotopietheorie erkläre nicht nur, weshalb «a gleich b» sei, sondern auch wie man von a nach b gelange. In der Mengenlehre müsste man diese Information zusätzlich definieren, was die Übersetzung von mathematischen Sätzen in die Programmiersprache erschwere, sagt Felder: «Die Hoffnung ist, dass man mit Wojewodskis Methode die Beweise direkter in der Programmiersprache übersetzen und effizienter verifizieren kann.»

Auf die Frage, ob sich Computer künftig gegen Menschen durchsetzen werden, wenn es darum geht, mathematische Beweise zu überprüfen, antworten Wojewodski und Felder offen. Wojewodski sagt: «Wir stehen noch ganz am Anfang einer langen Strasse des Wandels, und es ist unmöglich, heute zu sagen, wohin sie uns führt.» Felder sagt: «Computer können Fehler machen. Menschen können Fehler machen. Sicher ist nur, dass die Mathematik komplexer wird und das Beweisen nicht einfacher.»