Vor einigen Jahren hatten wir hier mal zu den neuen Möglichkeiten der Computer-Verifikation mathematischer Beweise geschrieben (Was ist ein Beweis?). Das Thema hat sich inzwischen weiterentwickelt, u.a. gab es am IAS in Princeton ein thematisches Jahr 2012/13 über die “univalenten Grundlagen der Mathematik”, aus dem auch ein Buch hervorgegangen ist, und natürlich gab es einige neue mit Computern überprüfte Beweise, z.B. den zum Satz von Feit und Thompson, einem wesentlichen Schritt in der Klassifikation der endlichen einfachen Gruppen. (Es handelt sich um den Satz, dass Gruppen ungerader Ordnung auflösbar sind.)
Vor einigen Wochen überraschte die Meldung, dass das US-Verteidigungsministerium 7,5 Mio Dollar für ein Forschungsprogramm (geleitet von Awodey, unter Beteiligung von u.a. Voevodsky) zur automatischen Beweisverifikation (“to reshape the foundations of mathematics by developing a new approach that allows for large-scale formalization and computer verification”) bereitstellt. Für die Verhältnisse der Mathematik ist das ungewöhnlich viel Geld, das höchste deutsche Stipendium, der Leibnizpreis, hat z.B. nur 2,5 Mio Euro. (Früher in den 80ern war militärfinanzierte Forschung noch ein Thema für erhitzte Diskussionen, besonders W.P.Thurston hatte sich damals als öffentlicher Kritiker exponiert, heute scheint dieser Aspekt in der reinen Mathematik kein Diskussionsthema mehr zu sein, anders als etwa bei Diskussionen über die NSA.)
Natürlich muß man sich keine Sorgen um das Berufsbild des Mathematikers machen: die Computer werden den Mathematikern nicht das Finden der Beweise, sondern nur deren Überprüfung abnehmen können. (Trotzdem könnten sich da neue Berufsbilder ergeben: Mathematiker brauchen in Zukunft vielleicht Helfer, die Beweise in formale, computerlesbare Sprache übertragen.)
Aus Topologen-Sicht bemerkenswert ist, dass die neuen Ansätze ein ursprünglich aus der Topologie stammendes Konzept benutzen, nämlich den auf Quillen zurückgehenden Begriff der Modellkategorie. Während der Begriff innerhalb der Topologie eher eine zusätzliche Abstraktion bzw. Axiomatisierung der Homotopietheorie war, scheint er hier nun auf einem ganz anderen Feld Anwendung zu finden, denn (aus Gründen, die ich nicht verstehe) ist es anscheinend sinnvoll, “Typen” (also Klassen von Objekten) nicht als Mengen, sondern als Homotopietypen aufzufassen. Einen gewissen Eindruck vermittelt vielleicht der ältere Artikel Voevodsky’s Univalence Axiom in Homotopy Type Theory. Ich verstehe bisher noch nicht, was dort eigentlich gemacht wird, oder wo z.B. in dieser Berechnung der Fundamentalgruppe des Kreises eigentlich die Topologie versteckt ist (“Prove that the total space { x : circle & circle_cover x } of the putative universal cover is contractible. I found it easiest to do this by using the fact that int is a set.” ).
Einen populärwissenschaftlichen Artikel (auf französisch) hat Images des Mathematiques: À la croisée des fondements des mathématiques, de l’informatique et de la topologie.
Kommentare (2)