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 (6)

  1. #1 Dirk Freyling
    Erde
    8. Mai 2022

    “Computerbewiesen” respektive “Computerbeweis” ist in sich ein Widerspruch. Da der Computer zuvor von “Menschenhand” (selektiv) mit Algorithmen “gefüttert” wurde um den Beweis durchzuführen.

    Mathematische Beweise sind eh mit äußerster Vorsicht zu genießen, sofern man die reale Welt abbilden möchte.

    Siehe unstrittig das Banach-Tarski-Paradoxon [BTP], welches im Ergebnis, mathematisch „axiomatisch sauber“, begründet, in der Realität kläglich scheitert.

    In einfachen Worten „beweisen („mathematisch)“ 1924 Stefan Banach (1892 -1945 polnischer Mathematiker) und Alfred Tarski (1901 – 1983 polnisch-amerikanischer Mathematiker und Logiker), wie aus einer Kugel zwei Kugeln werden. Das bedeutet, die mathematisch definierte „axiomatische Wirklichkeit“ besitzt hier [BTP] keine physische Realität.

  2. #2 Thilo
    8. Mai 2022

    Das Banach-Tarski-Paradoxon folgt letztlich aus dem Auswahlaxiom. Man kann dann darüber diskutieren, ob dieses physikalische Realität ist. Letztlich wird man das glauben müssen oder nicht. https://mathoverflow.net/questions/260057/axiom-of-choice-banach-tarski-and-reality

  3. #3 Frank Wappler
    9. Mai 2022

    Thilo schrieb (7. Mai 2022):
    > Formalisierung der Mathematik – wann führen Computer die Beweise?
    > Diese in letzter Zeit häufig diskutierte Frage […]

    > […] dass Lean […] besonders geeignet war, weil die Community zuvor bereits zahlreiche Grundlagen […] in Lean formalisiert hatte

    Man darf gespannt sein, wann die Formalisierung der Physik häufiger diskutiert wird,
    und wie eine geeignete (womöglich noch zu bildende) Community zumindest eine diskutable Auswahl entsprechender Grundlagen in Lean formalisieren würde.

  4. #4 Dr. Webbaer
    10. Mai 2022

    Nur im Denkmöglichen ergänzt :

    Es ist denkmöglich, dass ein mathematischer Beweis, der also auf mathematische Axiomatik zurückgeführt wird, so bewiesen wird : maschinell beigebracht wird, ohne dass dies ein wie gemeintes erkennendes Subjekt je (genau) verstehen kann.

    Sicherlich kann diese Idee, nicht Allen gefallen. [1]

    Im Spieltheoretischen ist so längst beigebracht, bspw. in einigen Brett- und Kartenspielen.
    (Ja, auch dies ist Mathematik, sehr strenge Mathematik sogar, weil sie über Regelmengen stark eingegrenzt ist und keiner (denkbarerweise : zweifelhaften) Axiomatiken bedarf.)

    Mit freundlichen Grüßen
    Dr. Webbaer

    [1]
    Sog. Schönheit ist im Mathematischen etwas für die anderen ?

  5. #5 Dr. Webbaer
    10. Mai 2022

    “Dass wir Menschen sagen, dass wir weiterhin gebraucht werden, aber dieser Aspekt ist, glaube ich, einsehbar, Ästethik dem Computer beizubringen, ist natürlich eine ganz andere Geschichte, Erika, wie siehst Du das, wie weit sind wir mit der Ästhetik, und dem Computer, finden, das was Michael sagt, dem Computer wirklich beibringen, dass etwas schön ist in der Mathematik?”
    (Eine, wie Dr. Webbaer findet : destastriöse Antwort einer Dame folgt, no problemo hier.)

    Mit freundlichen Grüßen
    Dr. Webbaer (der immer streng gegen Quoten auf Grund von biologisch bestimmbarerer Messbarkeit war)

  6. #6 Dr. Webbaer
    10. Mai 2022

    *
    desaströs