Diese in letzter Zeit häufig diskutierte Frage war das Thema einer Diskussionsrunde auf der Bonner Mathenacht am vergangenen Wochenende. Teilnehmer waren Peter Scholze, der Logiker Peter Koepke, die Informatikerin Erika Ábrahám und der Professor für Wissensrepräsentation Michael Kohlhase. Scholze erzählt, dass er durch das Liquid Tensor Experiment nicht nur Sicherheit über die Korrektheit, sondern auch ein besseres Verständnis des Beweises gewonnen habe, und dass Lean für den Beweis besonders geeignet war, weil die Community zuvor bereits zahlreiche Grundlagen (homologische Algebra, Banachräume, …) in Lean formalisiert hatte. Andere Computerbeweiser haben umfangreiche Bibliotheken zu anderen Gebieten, etwa Coq für Gruppentheorie (mit Blick auf den Satz von Feit-Thompson) oder HOL Light für Kugelpackungen. Kohlhase meint, dass etwa der Beweis der Klassifikation endlicher einfacher Gruppen inzwischen zu komplex sei, um von einem einzelnen Menschen verstanden zu werden, man also Computer brauche, während Ábrahám warnt, dass wir jetzt Sachen machen könnten, die wir selber nicht verstehen. Der Logiker Koepke sieht die Vision einer spielerischen Beschäftigung mit Mathematik: man bekomme beim Beweisen eine sofortige Rückmeldung, wodurch Mathematikangst überwunden werden könnte.
Kommentare (7)