Hier ist eine wichtige Frage, mit der wir uns zunehmend auseinandersetzen müssen, da KI-für-Mathematik-Pipelines alltäglicher werden: Warum ist es uns wichtig, schwierige Probleme zu lösen? Fast immer ist die Antwort *nicht*, weil wir besonders wollen, dass das schwierige Problem gelöst wird. (1/12)
David Budden
David Budden5. Jan., 22:14
Ich weiß wirklich nicht, warum das gesagt werden muss, aber können wir alle aufhören, so zu tun, als wäre eine fehlerhafte Zeile in einem mathematischen Beweis von Natur aus katastrophaler als eine fehlerhafte Zeile Code? Sicher. Einige sind es. Ich würde (metaphorisch!!!!) wetten, dass die mediane veröffentlichte mathematische Arbeit > 0 Fehler hat. Ohne das zu invalidieren.
Fragen wie die Existenz global glatter Lösungen der Navier-Stokes-Gleichungen sind von mathematischem Interesse, nicht weil die Antwort selbst schrecklich wichtig ist, sondern weil wir Grund zu der Annahme haben, dass der Prozess des *Entdeckens* der Antwort sehr wahrscheinlich ist... (2/12)
...um tiefere neue Einblicke in die Analyse, PDEs, Strömungsdynamik usw. zu gewinnen, mit neuen Techniken, die es auszunutzen gilt. Die Lösung von Fermat gab uns (indirekt) das Langlands-Programm. Die Lösung des Poincaré gab uns den Ricci-Fluss. Man hofft, dass die Lösung der Navier-Stokes-Gleichungen uns etwas ebenso Monumentales bringt. (3/12)
In der Tat identifizieren wir solche Probleme als "interessant schwierig", genau weil wir intuitiv annehmen, dass sie eine "Lücke" in unserem aktuellen Verständnis und unseren Methoden darstellen. Das ist der Grund, warum Spinner, die behaupten, (sagen wir) die Riemann-Hypothese mit "Tricks" oder elementaren Methoden zu lösen... (4/12)
...verfehlen etwas den Punkt: Wenn sich eines dieser großen Probleme als mit nur bestehenden mathematischen Erkenntnissen und Technologien lösbar herausstellen würde, wäre das eine immense Enttäuschung: Eine Quelle, von der wir zuvor dachten, sie sprudle, ist in Wirklichkeit trocken. (5/12)
Was hat das mit AI zu tun? Nun, wenn man die Prämisse akzeptiert, dass schwierige Probleme hauptsächlich interessant sind, weil sie neue Einsichten und Verständnis liefern, wirft das die Frage auf (im Lichte der Entwicklungen im Bereich AI): Wer ist für den "Verständnis"-Teil verantwortlich? (6/12)
Nehmen Sie Beweise durch Erschöpfung (wie im Vierfarbenproblem), die lange als etwas umstritten angesehen wurden, weil sie den Teil der "epistemischen Sicherheit" eines Beweises liefern, ohne notwendigerweise einen Teil des "Einblicks" zu liefern (was normalerweise das ist, was uns interessiert) (7/12)
Insofern sind Beweise durch Erschöpfung sicherlich nicht "falsch", aber sie sind in gewissem Sinne "betrügerisch" oder vielleicht "selbstzerstörerisch": Sie schließen ein potenziell fruchtbares Problem aus, während sie genau die Aspekte der Mathematik ausblenden, die sie interessant und lohnenswert machen. (8/12)
Ich denke, dass KI-generierte Beweise, in Abwesenheit eines Verständnisses oder Einblicks seitens des Menschen, der sie erstellt hat, ähnlich betrachtet werden sollten. Wenn Sie einen Lean-Beweis eines großen Theorems automatisch generieren, ist das großartig! Aber warum haben Sie das getan? (9/12)
Wenn Sie die neuen Erkenntnisse/Methoden, die der Beweis enthält, nicht verstehen, dann haben Sie lediglich die intellektuelle Last von sich selbst auf diejenigen verschoben, die bereit sind, ihn zu lesen und zu verstehen (und hoffentlich die darin enthaltenen Erkenntnisse an andere zu kommunizieren). (10/12)
Mathematik ist letztlich ein menschliches Kulturartefakt (wahrscheinlich unser tiefstes, reichhaltigstes und ältestes). Das Lösen schwieriger Probleme sollte nur ein *Proxy* sein, um dieses Artefakt zu erweitern. KI macht es aufregend einfach, neue Wege des mathematischen Verständnisses zu generieren.. (11/12)
...innerhalb dieses Artefakts, aber es macht es auch einfacher als je zuvor, den Proxy zu erreichen (d.h. schwierige Probleme zu lösen), während der ganze Grund, warum wir uns ursprünglich darum gekümmert haben, verloren geht (d.h. unser Verständnis zu vertiefen). Bitte mach das nicht. (12/12)
253