Verifikation von Beweisen und Software mit neuer Mathematik

Philosophisch betrachtet ist Wahrheit ein schwer zu fassender Begriff. In der Mathematik erlauben Beweise in einem formalen Kalkül mit Axiomen und logischen Schlussregeln, die Wahrheit von Aussagen zu überprüfen.

Wie Kurt Gödel und Alfred Tarski gezeigt haben, treten jedoch in jedem formalen Kalkül, der die Arithmetik beschreiben kann, systematisch unentscheidbare Aussagen auf. Deren Wahrheitsgehalt kann allerdings durch einen Beweis in einem ausgewählten erweiterten Metakalkül entschieden werden. In der Mathematik läuft also alles auf Beweise hinaus.

Vollständige Beweise mathematischer Theoreme sind häufig lang und komplex. Ihre Korrektheit ist daher schwer zu überprüfen. Dazu gehören berühmte Theoreme wie die Lösung der Fermatschen Vermutung, der Beweis des Vier-Farben-Satzes, das Feit-Thompson-Theorem oder die Lösung der Kepler-Vermutung. Es ist daher sinnvoll, solche Beweise (und übrigens auch Computerprogramme) auf die korrekte Anwendung der Schlussregeln des formalen Kalküls zu überprüfen. Dafür eignet sich hervorragend die sogenannte abhängige Typentheorie von Per Martin-Löf, eine Weiterentwicklung einiger Ideen von Bertrand Russell. In solchen Kalkülen werden Beweise zu Elementen in entsprechenden abhängigen Typen, die es zu konstruieren gilt. Bereits Gottfried Wilhelm Leibniz hatte unter dem Begriff Lingua Universalis ähnliche visionäre Ideen verfolgt.

Der mit der Fieldsmedaille ausgezeichnete Mathematiker Vladimir Voevodsky hat zusammen mit anderen die abhängige Typentheorie zur sogenannten Homotopy Type Theory weiterentwickelt, nachdem er auf einen versteckten Fehler in einer seiner Arbeiten hingewiesen wurde. In dieser Theorie werden alle Typen mit einer intuitiven topologischen Interpretation versehen. Der von Per Martin-Löf eingeführte Identitätstyp und ein neuer Äquivalenztyp stellen sich darin als wertvoll heraus, da sie den traditionellen Gleichheitsbegriff raffiniert so weit verallgemeinern, dass auch topologische Deformationen darin enthalten sind.

Abhängige Typentheorien können in digitalen Beweisassistenten realisiert werden, von denen es mittlerweile eine Vielzahl gibt. Sie bestehen aus Computerprogrammen, in denen Typen und ihre Schlussregeln beschrieben werden können. Der Beweis des Feit-Thompson-Theorems wurde 2012 durch Georges Gonthier mit dem Beweisassistenten COQ verifiziert. Der von Tom Hales gegebene Beweis der Kepler-Vermutung in der Programmiersprache OCAML wurde 2018 von ihm selbst mit ISABELLE/HOL validiert. Der Beweis des Vier-Farben-Satzes wurde 2005 von Georges Gonthier mit COQ überprüft. Ein neueres Beispiel ist ein Satz von Dustin Clausen und unserem Akademiemitglied Peter Scholze (ebenfalls ein Träger der Fieldsmedaille) aus ihrer 2019 entstandenen Theorie der sogenannten kondensierten Mathematik. Sie kontaktierten die Community um den Beweisassistenten LEAN, um den Beweis abzusichern. Dies gelang 2022 einer Gruppe um Johan Commelin und wurde Liquid-Tensor-Experiment genannt.

In der Zukunft werden Beweisassistenten im Zusammenspiel mit Computeralgebrasystemen, künstlicher Intelligenz und Repositorien unsere Arbeitsweise, Lehre und Publikationskultur entscheidend verändern. Gleichzeitig wird die Typentheorie an Bedeutung gewinnen. Eine spannende Zeit für die Mathematik und ihre Anwendungen!

(Stefan Müller-Stach)