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.?