WEBVTT NOTE PGD051 – automatic transcript (Whisper large-v3, wav2vec2 alignment, Sortformer + speaker embeddings). Generated by tools/transcribe/pi3tx.py, may contain errors. 00:00:00.261 --> 00:00:01.786 Okay, na dann fangen wir mal an. 00:00:01.786 --> 00:00:02.990 Hier ist wieder Pi ist genau 3. 00:00:02.990 --> 00:00:06.166 Mit euren, ihren, duzen wir eigentlich unsere Hörerinnen, Petra? 00:00:06.166 --> 00:00:07.986 Ich glaube, wir haben die bisher immer geduzt. 00:00:07.986 --> 00:00:09.627 Okay, mit euren Hosts. 00:00:09.627 --> 00:00:10.222 Petra Schwer, hallo. 00:00:10.222 --> 00:00:12.221 Und Thomas Kahle, hallo. Hi Thomas. 00:00:12.702 --> 00:00:15.212 Wir hatten schon wieder ein Jubiläum, Petra. 00:00:15.212 --> 00:00:16.621 Hast du es mitbekommen? Ich denke mal, du hast es mitbekommen. 00:00:16.621 --> 00:00:18.700 Ich habe es mitbekommen. Ich habe es auf Twitter gelesen. 00:00:18.700 --> 00:00:22.068 Hast du auf Twitter gelesen? Wir sind zwei Jahre alt geworden, genau. 00:00:22.068 --> 00:00:25.276 Am 3. April habe ich mir jetzt mal meinen Geburtstagskalender eingetragen. 00:00:25.276 --> 00:00:28.842 Am 3. April hat… Pi ist genau 3, immer Geburtstag. 00:00:28.842 --> 00:00:31.654 Und es ist jetzt zwei Jahre her, unsere erste Folge. 00:00:31.884 --> 00:00:35.007 Genau, Jubiläum auf Jubiläum. Mal gucken, was man da alles noch feiern kann. 00:00:35.007 --> 00:00:37.109 Also wenn wir Primzahlen feiern und Rundezahlen 00:00:37.109 --> 00:00:40.332 und dann noch so Jahresgeburtstage, dann wird das hier eine Riesenparty. 00:00:40.332 --> 00:00:42.663 Dann können wir eigentlich nur noch feiern, genau. 00:00:42.714 --> 00:00:44.435 Aber es gibt auch nichts Besonderes, was wir jetzt machen, 00:00:44.435 --> 00:00:46.687 weil eine Feier ist, außer dass wir sagen, dass heute eine Feier ist. 00:00:46.797 --> 00:00:49.639 Letztes Mal haben wir ja auch nichts gemacht, außer virtuell Konfetti geworfen. 00:00:49.639 --> 00:00:50.139 Naja. 00:00:50.822 --> 00:00:52.260 Und du hast heute das Thema für uns, stimmt's? 00:00:52.260 --> 00:00:54.007 Ich habe ein Thema mitgebracht, 00:00:54.007 --> 00:00:56.921 das mir gleich dreimal begegnet ist innerhalb der letzten paar Wochen. 00:00:56.921 --> 00:00:59.662 Und da dachte ich, das ist ein Wink nicht nur mit dem Zaunpfahl, 00:00:59.673 --> 00:01:01.108 sondern mit dem ganzen Gartenzaun. 00:01:01.242 --> 00:01:03.210 Deshalb habe ich das jetzt mitgebracht, auch auf die Gefahr hin, 00:01:03.210 --> 00:01:05.561 dass ich dir dein Thema für nächste Woche damit klaue. 00:01:05.561 --> 00:01:09.540 Was dann aber nur bewirkt, dass du hoffentlich auch ein bisschen was darüber weißt. 00:01:09.540 --> 00:01:10.241 Das ist ein Thema, 00:01:10.241 --> 00:01:14.164 von dem mir ein Kollege auf einer Konferenz vor kurzem ganz begeistert erzählt 00:01:14.164 --> 00:01:18.017 hat, weil er da einen Artikel dazu gelesen hat bei Quanta-Magazin. 00:01:18.287 --> 00:01:22.230 Gleichzeitig ist mir ein altes Heft von dem DMV-Jahresbericht in 00:01:22.230 --> 00:01:22.931 die Hände gefallen, 00:01:22.931 --> 00:01:24.632 wo vor einem Jahr dazu ein Thema, 00:01:24.632 --> 00:01:31.507 ein Artikel drin war, so ein Übersichtsartikel von der Angeliki Kutsuko-Agiaki. 00:01:31.898 --> 00:01:33.960 Falls du dich noch an diesen Artikel erinnerst. 00:01:33.960 --> 00:01:34.500 Ich glaube ja. Ja. 00:01:35.101 --> 00:01:37.125 Und es gab eine Bitte einer Hörerin, 00:01:37.125 --> 00:01:39.540 und spätestens jetzt solltest du wissen, worüber ich reden will, 00:01:39.671 --> 00:01:42.297 die uns aufgefordert hat, dazu mal was zu machen. 00:01:42.297 --> 00:01:43.860 Was könnte das Thema sein? 00:01:43.860 --> 00:01:45.621 Computerbeweissystem, stimmt's? 00:01:45.621 --> 00:01:48.326 Genau. Ich will das erzählen über formale Beweise 00:01:48.326 --> 00:01:51.051 und über diese automatischen Theorembeweiser, 00:01:51.051 --> 00:01:55.725 die seit einiger Zeit zunehmend an Bedeutung gewinnen, würde ich mal sagen. 00:01:55.725 --> 00:01:57.561 Ja, prima. Ich liebe Computer, weißt du ja. 00:01:57.561 --> 00:02:00.491 Ja, weiß ich, genau. Hast du schon mal ein bisschen, du kennst diesen Artikel, 00:02:00.491 --> 00:02:02.880 also weil du gesagt hast, ja, du glaubst, du erinnerst dich daran. 00:02:02.880 --> 00:02:05.544 Ich habe den Artikel schon mal gelesen 00:02:05.544 --> 00:02:08.018 und wollte immer mal so eine Bachelorarbeit machen, 00:02:08.249 --> 00:02:10.412 wo jemand das mal wirklich ausprobiert, also das Moderne. 00:02:10.412 --> 00:02:13.236 Ich habe das auch mal ausprobiert vor einem Jahrzehnt oder so 00:02:13.236 --> 00:02:15.890 oder noch mehr, aber da hat sich bestimmt einiges getan. 00:02:16.143 --> 00:02:17.761 Aber bisher hat es noch nie mal angebissen. 00:02:17.761 --> 00:02:20.707 Genau, da war auch mein spontaner Gedanke, als ich das Ding gelesen habe, 00:02:20.707 --> 00:02:21.208 dass ich so, oh, 00:02:21.208 --> 00:02:24.214 ich will unbedingt irgendeine Abschlussarbeit dazu mal ansetzen, 00:02:24.214 --> 00:02:27.830 dass sich einer das mal installiert und mal guckt, was man damit machen kann. 00:02:27.882 --> 00:02:30.588 Genau, die Geschichte von Quantamagazin, von der ich erzählt bekommen habe, 00:02:30.588 --> 00:02:31.730 mit der will ich vielleicht mal anfangen, 00:02:31.730 --> 00:02:34.958 weil die total spannend ist und eigentlich auch zeigt sozusagen, 00:02:34.958 --> 00:02:37.893 was die aktuelle Bedeutung von diesen Sachen ist. 00:02:38.064 --> 00:02:42.532 Da hat nämlich im Dezember 2020 Peter Scholze auf dem 00:02:42.532 --> 00:02:47.470 Blog Xena Project von Kevin Buzzard eine Challenge vorgeschlagen. 00:02:48.261 --> 00:02:52.665 Er hat nämlich zusammen mit seinem Kollegen Clausen einen Satz bewiesen, 00:02:52.665 --> 00:02:56.828 wo er sich nicht hundertprozentig sicher war, ob der Beweis korrekt ist. 00:02:56.828 --> 00:03:00.321 Er hat gesagt, das war der schwierigste Beweis, den er jemals so geführt hat. 00:03:00.532 --> 00:03:01.813 Und er war einfach nicht in der Lage, 00:03:01.813 --> 00:03:03.104 diesen kompletten Beweis 00:03:03.594 --> 00:03:07.548 vollständig in seinem Kopf als Ganzes zu durchdringen und wollte eben, 00:03:07.758 --> 00:03:10.330 dass dieser Beweis formalisiert wird. 00:03:11.280 --> 00:03:15.046 Aktuelle Forschungsmathematik sozusagen von jetzt hat er eben 00:03:15.046 --> 00:03:20.795 ausgesetzt als Projekt für diese formalen Theorembeweiser mit der Bitte, 00:03:20.795 --> 00:03:24.060 doch diesen Beweis einmal zu verifizieren. 00:03:24.060 --> 00:03:25.672 Und dann gab es eine ganz lustige 00:03:25.762 --> 00:03:28.735 Diskussion auch in den Kommentaren zu dem Blogartikel, 00:03:29.046 --> 00:03:31.479 wo jemand wissen wollte, was denn mit einer Lösung passiert. 00:03:31.589 --> 00:03:33.661 Also wie die veröffentlicht werden soll, 00:03:33.671 --> 00:03:36.395 ob man dann ein gemeinsames Paper mit Scholze schreiben darf, 00:03:36.395 --> 00:03:41.230 wenn man das umgesetzt hat oder was da sozusagen das Vorgehen sein wird. 00:03:41.760 --> 00:03:46.444 Und da hat Kevin Buzzard, also der eben großer Pionier ist, würde ich mal sagen, 00:03:46.444 --> 00:03:50.237 und auch da diese Lean-Machine sehr vorantreibt, 00:03:50.628 --> 00:03:53.080 geantwortet auf diesen Kommentar, 00:03:53.550 --> 00:03:55.912 dass er denkt, dass die große Frage nicht ist, 00:03:55.912 --> 00:03:58.515 was mit dem Code passiert, falls man das verifiziert, 00:03:58.515 --> 00:04:00.246 sondern dass die große Frage ist, 00:04:00.596 --> 00:04:05.070 ob das überhaupt möglich ist, dieses Theorem zu verifizieren. 00:04:05.981 --> 00:04:07.636 Und dann, spannenderweise, 00:04:07.788 --> 00:04:11.300 gab es ein halbes Jahr später einen neuen Blogpost von Scholze, 00:04:11.300 --> 00:04:14.733 wo er eben beschreibt, dass das schon passiert ist. 00:04:14.843 --> 00:04:16.925 Also, dass der wesentliche Schritt von dem Beweis, 00:04:16.925 --> 00:04:19.767 wo er sich eben unsicher war, dass der schon umgesetzt ist. 00:04:19.767 --> 00:04:22.730 Also nicht der komplette Satz, aber sozusagen die Bausteine, 00:04:22.730 --> 00:04:27.283 die er für kritisch gehalten hat, dass die eben jetzt verifiziert sind. 00:04:27.694 --> 00:04:29.856 Und dass er tatsächlich daraus gelernt hat, 00:04:29.856 --> 00:04:32.018 also Scholze selbst, warum der Beweis funktioniert. 00:04:32.018 --> 00:04:35.210 Also, was es ausmacht, dass dieser Beweis tatsächlich … 00:04:35.280 --> 00:04:38.863 klappt, so wie er klappt. Ja, und das fand ich sehr bemerkenswert. 00:04:38.863 --> 00:04:43.046 Also, dass nicht nur die Experten sich nicht wirklich sicher waren, 00:04:43.046 --> 00:04:44.537 ob das überhaupt möglich ist. 00:04:45.288 --> 00:04:46.048 Dann die Tatsache, 00:04:46.048 --> 00:04:49.601 dass es nach einem halben Jahr schon geklappt hat und der, 00:04:49.711 --> 00:04:51.462 von dem der Beweis eigentlich stammt, 00:04:51.612 --> 00:04:55.035 daraus tatsächlich erst nach eigenen Aussagen gelernt hat, 00:04:55.035 --> 00:04:56.236 wieso der Beweis funktioniert. 00:04:56.236 --> 00:04:59.848 Ich habe das, wenn ich Studierenden manchmal so was mitgebe, 00:04:59.959 --> 00:05:01.960 dann ist es auch oft so dieses, man eigentlich … 00:05:01.960 --> 00:05:05.206 … auch in der Forschungsmathematik nicht so richtig hundertprozentig sicher 00:05:05.206 --> 00:05:06.718 ist, ob der Beweis jetzt richtig ist. 00:05:06.929 --> 00:05:09.944 Also das ist bei denen so ein falscher Eindruck, den man von Übungsaufgaben kriegt. 00:05:10.075 --> 00:05:13.160 Man macht seine Übungsaufgaben und dann kriegt man die Lösung. 00:05:13.160 --> 00:05:16.008 Und dann weiß man bei jeder Entscheidungsfrage, 00:05:16.008 --> 00:05:18.354 stimmt das oder stimmt das nicht, da gibt es dann irgendwen Schlaues, 00:05:18.354 --> 00:05:20.662 der sagt, ja stimmt, hattest du richtig. 00:05:20.662 --> 00:05:23.591 Und in der Forschungsmathematik, man beweist sowas, 00:05:23.591 --> 00:05:27.050 aber bei manchen Sachen ist man sich wirklich richtig sicher. 00:05:27.122 --> 00:05:29.499 Aber richtig sicher heißt vielleicht 99,9 Prozent. 00:05:29.790 --> 00:05:32.026 Und bei manchen Sachen ist man sich nur 99,0 Prozent sicher. 00:05:33.423 --> 00:05:34.516 Und bei manchen Sachen, 00:05:34.869 --> 00:05:38.581 da prüft man die schon fast so auf so einem formalen Weg, 00:05:38.581 --> 00:05:41.884 traut sich aber noch nicht zu sagen, ich habe verstanden, wie der Beweis geht. 00:05:41.884 --> 00:05:45.046 Man hat einen formalen Beweis gefunden und prüft den nach und es passt so von 00:05:45.046 --> 00:05:48.929 der Logik. Aber dass man irgendwie so ein Verständnis hat, hat man nicht. 00:05:48.929 --> 00:05:50.360 Und dann ist natürlich jetzt so ein, 00:05:50.531 --> 00:05:54.244 wenn es wirklich ein Computer prüfen kann, ist das ein schöner, schöner Schluss. 00:05:54.254 --> 00:05:57.166 Aber hatten die das nicht auch irgendwie nach so einer Musikband benannt oder sowas? 00:05:57.196 --> 00:05:58.807 Das Projekt? Gab es da nicht irgend so einen Witz? 00:05:58.818 --> 00:06:01.290 Das Projekt heißt The Liquid Tensor Experiment. 00:06:01.290 --> 00:06:01.909 Perimen. 00:06:02.143 --> 00:06:03.749 Ja, genau. Da gibt es so eine experimentelle Musikband, 00:06:03.749 --> 00:06:06.349 die sich ganz interessant anhört, meine ich. 00:06:06.582 --> 00:06:09.572 Ja, da gibt es noch mehr so Musikanspielungen. 00:06:09.572 --> 00:06:11.098 Ich werde mal diesen Blogpost auch verlinken. 00:06:11.098 --> 00:06:14.292 Da gibt es so Subunterschriften in der Art und Weise, 00:06:14.292 --> 00:06:18.439 wo das eben erklärt wird, was der Satz ist, wie der Beweis funktioniert und so, 00:06:18.952 --> 00:06:20.407 was eigentlich gemacht werden soll. 00:06:20.478 --> 00:06:23.731 Und diese Kapitelunterschriften haben alle so Musikanspielungen. 00:06:23.731 --> 00:06:26.390 Okay. Also Liquid Tensor Theory. 00:06:26.442 --> 00:06:28.452 Liquid Tensor Experiment hieß es. 00:06:28.452 --> 00:06:30.041 Liquid Tensor Experiment, okay. 00:06:30.041 --> 00:06:32.935 Genau. Also es ist geglückt, das Experiment, würde ich sagen. 00:06:33.246 --> 00:06:36.531 Vielleicht können wir mal ein paar Sachen klären, ja? 00:06:36.531 --> 00:06:39.436 Ich denke, wir sollten klären, was ein formaler Beweis ist, 00:06:39.436 --> 00:06:42.122 wie das funktioniert, formale Beweise zu machen. 00:06:42.122 --> 00:06:43.927 Und ich würde auch gerne ein bisschen darüber reden, 00:06:43.927 --> 00:06:46.242 warum wir formale Beweise machen sollten. 00:06:46.673 --> 00:06:49.530 Fangen wir mal an mit, was ist ein formaler Beweis? 00:06:49.743 --> 00:06:51.301 Willst du was sagen? Soll ich was sagen? 00:06:51.301 --> 00:06:52.283 Naja, ich würde sagen, 00:06:52.283 --> 00:06:57.865 dieses Nachprüfen von Implikationen aus A folgt B oder aus A und B folgt C, 00:06:58.096 --> 00:06:59.620 das ist ja schon was, was ein Computer machen kann. 00:06:59.620 --> 00:07:03.180 Da denkt man sich ja irgendwie, naja, wenn ich das programmieren würde, 00:07:03.753 --> 00:07:06.021 könnte meine Logik zumindest überprüft werden. 00:07:06.021 --> 00:07:07.906 Also das Finden des Beweises ist vielleicht schwierig, 00:07:07.906 --> 00:07:11.114 aber das Überprüfen von so logischen Argumenten, 00:07:11.114 --> 00:07:13.630 das sollte doch wohl ein Computer machen können. 00:07:13.721 --> 00:07:15.764 Und das ist so ein formaler Beweis, 00:07:15.764 --> 00:07:16.726 das ist wahrscheinlich ein, 00:07:16.726 --> 00:07:19.070 würde ich jetzt mal in erster Approximation sagen, so ein Beweis, 00:07:19.070 --> 00:07:22.495 der so aufgeschrieben ist, in der Programmiersprache, die dazu passt, 00:07:22.495 --> 00:07:25.162 dass ein Computer prüfen kann, ob die Logik stimmt. 00:07:25.162 --> 00:07:27.188 Und bei einfachen Implikationen machen wir das ja auch, 00:07:27.188 --> 00:07:31.030 also irgendwie routinemäßig, algorithmisch, wenn man jetzt ein Paper liest. 00:07:31.141 --> 00:07:32.995 Diese Beweise, die Logik nachzuvollziehen. 00:07:33.106 --> 00:07:35.091 Aber es gibt eben so Fallstricke. 00:07:35.091 --> 00:07:37.879 Man sagt halt oft, okay, diese Fälle prüft man einfach nach. 00:07:37.879 --> 00:07:39.267 Also es gibt eben Teile, die fehlen, 00:07:39.267 --> 00:07:41.968 die man einfach weglässt aus sozialen Konventionen. 00:07:42.102 --> 00:07:43.486 Und es gibt Fallunterscheidungen. 00:07:43.486 --> 00:07:44.590 Man macht einfach so Statements. 00:07:44.590 --> 00:07:46.725 Ja, es genügt, folgende drei Fälle zu betrachten. 00:07:46.896 --> 00:07:48.362 Und in Wirklichkeit sind es vier. 00:07:48.362 --> 00:07:53.563 Und da könnte man sich vorstellen, dass dann, wenn man das programmieren muss, 00:07:53.915 --> 00:07:56.510 also wenn man einen Beweis formalisiert, 00:07:56.901 --> 00:08:00.632 man dann sich selbst eben zwingt, keine Abkürzungen zu nehmen, 00:08:00.632 --> 00:08:03.630 so wie man sie vielleicht auf Papier nehmen würde. 00:08:03.741 --> 00:08:05.665 Ja, das ist ein wesentlicher Punkt. 00:08:05.665 --> 00:08:07.809 Also du hast schon komplett richtig gesagt, 00:08:07.809 --> 00:08:11.116 so die Definition eines formalen Beweises ist eben ein Beweis, 00:08:11.116 --> 00:08:13.081 der aufgeschrieben ist in einer formalen Sprache. 00:08:13.081 --> 00:08:16.278 Man muss sich das tatsächlich so vorstellen wie so eine Programmiersprache. 00:08:16.590 --> 00:08:18.033 Also diese Beweise, wenn man die anguckt, 00:08:18.033 --> 00:08:21.100 die sehen auch ein bisschen so aus wie Programmiercode. 00:08:21.100 --> 00:08:23.255 Ja, also da gibt es so Kennwörter, 00:08:23.326 --> 00:08:24.569 die immer mal wiederkommen 00:08:24.569 --> 00:08:29.501 und auch so bestimmte Schlüsselrollen übernehmen in diesen formalen Beweisen. 00:08:29.501 --> 00:08:33.107 Kombiniert mit aussagenlogischen Verknüpfungen, 00:08:33.107 --> 00:08:37.334 also so und oder Verknüpfungen, Gleichungen oder dann eben Rechnungen, 00:08:37.334 --> 00:08:41.430 Quadrate, Summen, Produkte, solche Dinge. 00:08:41.781 --> 00:08:45.748 Es kann eben keine Prosa darin vorkommen mehr. 00:08:45.748 --> 00:08:47.452 Also man muss alles, 00:08:47.452 --> 00:08:51.040 was die Beweisschritte einzeln ausmacht, formalisiert aufschreiben. 00:08:51.040 --> 00:08:51.540 Man kann 00:08:52.880 --> 00:08:54.902 nicht mehr mit Anschauung argumentieren, 00:08:54.902 --> 00:08:58.516 was manchmal eben passiert, je nachdem, je nach Forschungsgebiet, 00:08:58.666 --> 00:09:02.680 wo man dann sagen kann, man kann sich vorstellen, dass im R³ das so und so aussieht. 00:09:03.251 --> 00:09:04.763 Das geht eben nicht mehr. 00:09:05.013 --> 00:09:08.277 Und es sind eben reine formale logische Schlüsse, 00:09:08.277 --> 00:09:11.710 die da eben deduktiv der Reihe nach sozusagen erfolgen. 00:09:11.801 --> 00:09:14.515 Wenn man das auf einem ganz reinen Level betreibt, 00:09:14.525 --> 00:09:18.061 muss eben jeder einzelne kleine Schritt explizit ausformuliert werden. 00:09:18.352 --> 00:09:22.780 Und es muss jedes Ding, was verwendet wird, auch vorhanden sein. 00:09:22.780 --> 00:09:27.816 Also es gibt so eine, je nachdem welchen Theorembeweiser man da nimmt, 00:09:27.987 --> 00:09:31.881 so vorimplementierte Bibliotheken mit Sätzen, die schon verifiziert sind. 00:09:32.032 --> 00:09:34.885 Die kann man selbstverständlich benutzen unterwegs 00:09:35.155 --> 00:09:39.290 und auch aufrufen wie so Funktionen in einem Computerprogramm. 00:09:39.701 --> 00:09:43.094 Es gibt aber auch Beweistechniken, die implementiert sind. 00:09:43.525 --> 00:09:46.137 Also solche kleinen Tools, 00:09:46.348 --> 00:09:49.371 die man benutzen kann, die so Standardbeweismethoden sind. 00:09:49.371 --> 00:09:51.974 Zum Beispiel Umformulierung von Gleichungen, 00:09:51.974 --> 00:09:54.016 algebraische Manipulationsregeln, 00:09:54.016 --> 00:09:57.590 wie zum Beispiel sowas wie Assoziativgesetz oder solche Dinge. 00:09:57.662 --> 00:10:00.487 All diese Regeln müssen mal implementiert worden sein 00:10:00.487 --> 00:10:01.489 von irgendeinem Mathematiker, 00:10:01.489 --> 00:10:02.561 können dann aber 00:10:02.912 --> 00:10:06.819 eben von Anwenderinnen halt auch aufgerufen und benutzt werden, ja, 00:10:06.819 --> 00:10:10.492 wie so eine Bibliothek in der Programmiersprache. 00:10:11.163 --> 00:10:14.165 Ja, also man führt im Prinzip eine mathematische Aussage durch so einen 00:10:14.165 --> 00:10:20.179 formalen Beweis auf Axiome zurück, ja, mit Zwischenschritten. 00:10:20.229 --> 00:10:23.672 Ja, und die Zwischenschritte müssen eben ziemlich explizit sein, 00:10:23.672 --> 00:10:27.254 dass wenn man, es ist jetzt eine kleine Rechnung, schreiben würde, 00:10:27.254 --> 00:10:29.926 dann muss diese Rechnung eben ausgeführt werden. 00:10:30.076 --> 00:10:31.287 Und die Frage ist, glaube ich, 00:10:31.377 --> 00:10:35.030 wie viele Tipps man dem Computerprogramm dann noch geben muss. 00:10:35.681 --> 00:10:38.076 Wie diese Rechnung auszuführen ist oder 00:10:38.187 --> 00:10:41.034 dass dann nur noch Sachen trivial bezeichnet werden können, 00:10:41.034 --> 00:10:42.921 die wirklich trivial sind. 00:10:42.921 --> 00:10:46.000 Ich glaube, da steckt so Optimierungssoftware irgendwie noch dahinter. 00:10:46.000 --> 00:10:48.811 Das erinnert mich an so einen interessanten Vortrag, 00:10:48.811 --> 00:10:50.703 den ich mal gehört habe über das Simplify-Command. 00:10:50.703 --> 00:10:53.518 Es gibt ja so Computeralgebra-Systeme, die irgendwie so ein Simplify-Command haben. 00:10:53.518 --> 00:10:54.907 Das ist eigentlich sehr interessant, 00:10:54.907 --> 00:10:57.120 da aus Informatikperspektive mal drüber nachzudenken. 00:10:57.120 --> 00:10:59.921 Hat irgendwie einen großen komplizierten Ausdruck. 00:10:59.921 --> 00:11:02.647 Und jetzt gibt es so ein magisches Kommando in, sagen wir mal, 00:11:02.647 --> 00:11:04.361 Mathematica oder Sage. 00:11:04.632 --> 00:11:08.142 Das soll Simplify heißen, das soll irgendwie den Ausdruck vereinfachen. 00:11:08.142 --> 00:11:11.229 Aber das ist ja eigentlich ein tierisch kompliziertes Optimierungsproblem. 00:11:11.229 --> 00:11:12.492 Wie soll man das formulieren? 00:11:12.492 --> 00:11:16.122 Muss man erstmal definieren, was ist ein einfacherer Ausdruck? 00:11:16.122 --> 00:11:18.789 Gibt es irgendwie eine Normalform für so einen Ausdruck? 00:11:18.789 --> 00:11:23.230 Also was für uns Menschen irgendwie offensichtlich erscheint. 00:11:23.562 --> 00:11:25.531 Hier, der Ausdruck sieht doch viel einfacher aus. 00:11:25.531 --> 00:11:27.710 Da ist dieser redundante Term weg. 00:11:27.825 --> 00:11:30.770 Wirklich zu programmieren ist tierisch kompliziert. 00:11:30.780 --> 00:11:36.090 Ja, ist aber auch subjektiv. Warum das eine einfacher aussieht als das andere. 00:11:36.090 --> 00:11:38.474 Der eine mag vielleicht kleine Nenner, der andere größere. 00:11:38.474 --> 00:11:42.162 Der nächste will möglichst das als Summe haben, der andere als Produkt. 00:11:42.162 --> 00:11:43.948 Ja, weil es ein Optimierungsproblem ist 00:11:43.948 --> 00:11:46.054 und verschiedene Leute verschiedene Funktionen optimieren, 00:11:46.054 --> 00:11:47.481 wenn sie ihre Terme vereinfachen. 00:11:47.481 --> 00:11:49.406 Ja, und man muss es aber präzisieren. 00:11:49.406 --> 00:11:53.136 Also wenn du Simplify schreibst, so was gibt es auch in diesen Theorembeweisern. 00:11:53.136 --> 00:11:54.750 Solche Kommandos, sage ich jetzt. 00:11:55.341 --> 00:11:57.063 Die eben Ausdrücke vereinfachen. 00:11:57.063 --> 00:12:01.378 Aber dann muss man eben formal definieren, was es bedeutet zu vereinfachen. 00:12:01.569 --> 00:12:05.062 Und auch das folgt einem festgelegten Algorithmus dann. 00:12:05.133 --> 00:12:08.286 Du hast Computeralgebra-Systeme erwähnt, was vielleicht noch wichtig ist, 00:12:08.757 --> 00:12:11.290 falls es dem einen oder anderen nicht klar sein sollte. 00:12:11.640 --> 00:12:14.745 Die würde ich ganz gerne wirklich abgrenzen von den Theorembeweisern. 00:12:14.745 --> 00:12:18.772 Ja, ein Computeralgebra-System, also sowas wie Mathematica, Maple, Matlab, 00:12:18.772 --> 00:12:20.024 was es da noch alles gibt. 00:12:20.094 --> 00:12:23.890 Mit denen kann man im Wesentlichen komplizierte Berechnungen durchführen. 00:12:24.161 --> 00:12:26.495 Das sind aber keine Theorembeweiser, 00:12:26.646 --> 00:12:30.894 weil die keine formal-logischen Schlüsse ziehen können 00:12:30.894 --> 00:12:33.340 und auch formal-logische Schlüsse nicht nachprüfen können. 00:12:33.340 --> 00:12:35.026 Ja, die können nachprüfen, 00:12:35.026 --> 00:12:39.770 ob eine Rechnung korrekt ist vielleicht oder Rechnungen korrekt durchführen. 00:12:39.963 --> 00:12:41.121 Aber das war es dann auch schon. 00:12:41.121 --> 00:12:43.869 Man braucht ja wahrscheinlich erstmal ganz schön viele Datentypen für 00:12:43.869 --> 00:12:47.902 die verschiedenen Arten von Aussagen, mit denen man zu tun hat. 00:12:47.902 --> 00:12:50.818 Also man hat ja, in der Mathematik hat man einfache Aussagen, 00:12:51.009 --> 00:12:52.634 so wie irgendeinen Satz, den man beweisen will, 00:12:52.634 --> 00:12:54.440 aber viele Aussagen sind ja so parametrisiert. 00:12:54.440 --> 00:12:57.360 Da hat man eine Aussage für jede natürliche Zahl, 00:12:57.974 --> 00:12:59.870 eine Aussage, also so ein Prädikat. 00:13:00.160 --> 00:13:03.686 Würde das dann in der Logik heißen und dann quantifiziert man darüber 00:13:03.686 --> 00:13:07.332 und sowas würde man in einem normalen Computeralgebra-System hat man ja 00:13:07.332 --> 00:13:11.300 gar nicht die Ausdrucksfähigkeit für ja so Prädikate. 00:13:11.300 --> 00:13:14.055 Da wird es auch gar nicht abgebildet. 00:13:14.506 --> 00:13:17.141 Also diesen Artikel, den ich da gelesen habe, 00:13:17.232 --> 00:13:21.450 der beschreibt diese Theorembeweis-Software Isabelle. 00:13:21.840 --> 00:13:25.985 Die kann zum Beispiel gleich mehrere logische Axiomensysteme abbilden, 00:13:25.985 --> 00:13:30.971 also Aussagen Logik 1. Stufe oder höherer Stufe, ZFC, solche Dinge. 00:13:30.971 --> 00:13:33.794 Also da kann man sich sozusagen auch entscheiden, 00:13:33.794 --> 00:13:37.287 in welchem logischen System man eben Sätze beweisen will. 00:13:37.498 --> 00:13:39.419 Also das ist halt auch eine Nein. 00:13:39.781 --> 00:13:42.690 Mächtigkeit, die die Theorembeweise haben, 00:13:42.690 --> 00:13:45.930 die aber in den Computeralgebra-Systemen gar nicht abgebildet sind. 00:13:46.262 --> 00:13:48.628 Aber man steht ja immer, auch wenn man ein normales Paper schreibt, 00:13:48.628 --> 00:13:51.625 was jetzt nicht formalisiert ist, so auf den Schultern von den Riesen 00:13:52.117 --> 00:13:53.309 und fängt irgendwo an. 00:13:53.543 --> 00:13:58.001 Also kann ich auch in so einem Theorembeweiser da anfangen, wo mein Paper anfängt? 00:13:58.001 --> 00:14:03.925 Du brauchst dann wahrscheinlich auch eine relativ lange Liste von Lämmerter 00:14:03.956 --> 00:14:06.964 oder Aussagen, die schon... vorher bewiesen wurden, 00:14:06.964 --> 00:14:08.448 die schon als richtig angenommen wurden. 00:14:08.448 --> 00:14:10.313 Aber ich muss sie zumindest trotzdem alle nochmal hinschreiben, 00:14:10.313 --> 00:14:12.926 weil ich meine Annahmen alle explizit machen muss. 00:14:12.926 --> 00:14:14.301 Ist das irgendwie so ein großer Teil der Arbeit? 00:14:14.301 --> 00:14:16.786 Da sprichst du einen sehr wichtigen Punkt an. 00:14:16.786 --> 00:14:19.011 Also eine Sache ist, wenn man wirklich seinen... 00:14:19.011 --> 00:14:20.394 also nimm dein letztes Paper, 00:14:20.394 --> 00:14:23.322 den wichtigsten Satz da draus und du willst den formal beweisen. 00:14:23.322 --> 00:14:25.709 Dann müsstest du theoretisch alles, 00:14:25.709 --> 00:14:29.480 was da reinfließt, auch formal beweisen oder schon als... 00:14:29.480 --> 00:14:32.552 als formal bewiesen in dieser Datenbank 00:14:32.823 --> 00:14:37.426 der schon formal verifizierten Theoreme wiederfinden. 00:14:37.426 --> 00:14:44.501 Ja, zurück bis jede kleinste Regel, Rechenregel aus der ganz elementaren Arithmetik. 00:14:44.652 --> 00:14:47.113 Ja, genau. Wenn man so ein elegantes Algebra-Paper hat, 00:14:47.113 --> 00:14:47.954 dann ist dann der Hauptsatz, 00:14:47.954 --> 00:14:51.357 der Beweis vom Hauptsatz ist immer zwei Zeilen und der geht dann irgendwie so. 00:14:51.357 --> 00:14:55.790 After lemma 4 7, this follows by combining theorem 5 with... 00:14:56.021 --> 00:14:59.893 Da ist ziemlich viel versteckt und man kann anhand dieses Beweises nichts von 00:14:59.893 --> 00:15:01.919 der Struktur verstehen. Ja, das ist genau der... 00:15:01.919 --> 00:15:04.622 Der Punkt. Es gibt aber noch eine Möglichkeit, 00:15:04.622 --> 00:15:06.003 wie man da so ein bisschen tricksen kann. 00:15:06.003 --> 00:15:07.864 Das hat natürlich auch so seine Fallstricke. 00:15:07.864 --> 00:15:12.577 Man kann jetzt relative Korrektheit überprüfen statt absolute Korrektheit. 00:15:12.808 --> 00:15:15.050 Wenn du zum Beispiel sicherstellen willst, 00:15:15.050 --> 00:15:18.222 dass einfach dein Paper in sich richtig ist, 00:15:18.472 --> 00:15:21.514 könntest du einfach alle Lämmer und Propositionen und Sätze, 00:15:21.514 --> 00:15:25.377 die in deinem Paper vorkommen, formal aufschreiben, die Beweise, 00:15:25.377 --> 00:15:29.310 und durch den formalen Beweis Checker prüfen lassen. 00:15:29.680 --> 00:15:32.345 Du wirst aber mit Sicherheit irgendwie mindestens eine Rechenregel 00:15:32.345 --> 00:15:35.901 oder einen Satz zitieren, den irgendjemand anders vorher schon mal bewiesen hat, 00:15:35.972 --> 00:15:40.669 der vielleicht nicht in dieser Datenbank ist, die schon komplett verifiziert ist. 00:15:40.861 --> 00:15:46.981 Solche Sätze kann man als zusätzliche Axiome seinem Theorienprüfer mitgeben 00:15:47.191 --> 00:15:49.705 und sagen, nimm mal an, diese Aussage ist richtig, 00:15:49.936 --> 00:15:52.079 ist dann der folgende Beweis formal richtig. 00:15:52.079 --> 00:15:54.914 Richtig. Also erst, mal ist es total gut, 00:15:55.026 --> 00:15:59.710 weil man eben auch lokal überprüfen kann, ob Mathematik korrekt ist. 00:16:00.200 --> 00:16:01.121 Es hat den Haken, 00:16:01.121 --> 00:16:04.756 dass man dann sozusagen den Stempel dran hat, 00:16:04.786 --> 00:16:07.459 dieser Beweis ist formal geprüft, 00:16:07.990 --> 00:16:10.743 aber man unter Umständen Sachen benutzt hat, 00:16:10.994 --> 00:16:11.855 die falsch sind, 00:16:11.855 --> 00:16:13.697 weil sie eben nicht formal geprüft sind 00:16:13.697 --> 00:16:15.961 und da sich ja auch noch Fehler verstecken können. 00:16:15.961 --> 00:16:18.727 Na gut, das ist ja ein klassisches Problem, was man immer mit der Mathematik hat. 00:16:18.727 --> 00:16:23.646 Also das ist nichts, was schlechter ist als in der vorformalisierten Welt, 00:16:24.118 --> 00:16:25.570 sondern einfach genauso. 00:16:25.620 --> 00:16:27.514 Also ich meine, genauso in meinem Paper, 00:16:27.565 --> 00:16:30.641 was ich normal mit Tech schreibe und mir selbst überlege, 00:16:30.852 --> 00:16:34.822 ob das richtig ist, nutze ich auch Sachen und habe nicht alle Theoreme. 00:16:34.822 --> 00:16:37.589 Wenn ich ein Theorem aus einem veröffentlichten Paper benutze, 00:16:37.589 --> 00:16:41.662 gehe ich davon aus, dass es halt Peer Review durchlaufen hat und korrekt ist. 00:16:41.662 --> 00:16:43.546 Und den Test der Zeit gibt es ja auch immer noch, 00:16:43.546 --> 00:16:47.776 denn wenn was nicht stimmt, ergeben sich daraus meistens Inkonsistenzen, 00:16:47.776 --> 00:16:49.861 die dann irgendwann auffallen. 00:16:49.861 --> 00:16:53.101 Kann natürlich lange dauern, vielleicht ist man noch nicht da, aber so ist es halt. 00:16:53.101 --> 00:16:56.632 Also es sind tatsächlich auch schon so kleinere Fehler in Sätzen, 00:16:56.632 --> 00:16:59.668 ich habe jetzt leider kein Beispiel fertig rausgesucht. 00:16:59.668 --> 00:17:00.396 Mit Formalisierung gefunden? 00:17:00.396 --> 00:17:02.146 Mit Formalisierung gefunden worden, genau, 00:17:02.146 --> 00:17:04.171 die man halt formalisiert hat und dann gemerkt hat, 00:17:04.171 --> 00:17:06.800 nee, diese Abschätzungskonstante ist halt ein bisschen falsch. 00:17:06.800 --> 00:17:11.136 Also es gibt eine, aber die sieht halt ein kleines bisschen anders aus, als die, 00:17:11.136 --> 00:17:12.063 die eigentlich da steht. Ja, 00:17:12.063 --> 00:17:12.846 ich könnte mir vorstellen, 00:17:12.846 --> 00:17:15.426 wenn man das jetzt auf großer Fläche ausrollen würde, 00:17:15.597 --> 00:17:19.422 dass man unglaublich viele kleine Probleme, 00:17:19.422 --> 00:17:23.295 kleine umschiffbare Probleme finden würde und es total undankbar ist, 00:17:23.485 --> 00:17:26.538 dass die Formalisiererinnen und Formalisierer 00:17:26.728 --> 00:17:30.631 dann die ganze Zeit so aufkehren müssen hinter so einer Dampfwalze, 00:17:30.631 --> 00:17:34.003 die da irgendwie durch ist, durch irgendwas Schwieriges. 00:17:34.294 --> 00:17:37.316 Und dann liegen da noch die ganzen Scherben rum und bevor es schön wird, 00:17:37.316 --> 00:17:38.957 muss irgendwer noch die Scherben aufkehren. 00:17:38.957 --> 00:17:41.159 Einer muss mal zusammenfegen noch. 00:17:41.159 --> 00:17:42.401 Klingt irgendwie undankbar. 00:17:42.401 --> 00:17:44.841 Aber vielleicht können es ja Computer machen, die diese ganzen undankbaren Sachen. 00:17:44.841 --> 00:17:47.328 Also im Moment arbeiten tatsächlich sehr viele Menschen daran, 00:17:47.328 --> 00:17:49.954 ganz viel Mathematik zu formalisieren 00:17:49.954 --> 00:17:52.022 und aus ganz unterschiedlichen Perspektiven auch. 00:17:52.022 --> 00:17:55.072 Es wird sowohl ganz elementare Mathematik formalisiert, 00:17:55.072 --> 00:17:57.810 die jetzt zum Beispiel so in den Grundvorlesungen drankommt. 00:17:57.863 --> 00:18:00.681 Manchmal nutzt man das auch zu Unterrichtszwecken. 00:18:00.681 --> 00:18:02.855 Also man lässt Studierenden in den 00:18:03.207 --> 00:18:06.053 frühen Semestern auch Beweise von den Sätzen, 00:18:06.053 --> 00:18:09.461 die sie eben gerade in ihren Anfängervorlesungen gesehen haben. 00:18:09.461 --> 00:18:13.491 Formalisieren, um eben ein besseres Verständnis davon zu gewinnen, 00:18:13.491 --> 00:18:16.841 was eigentlich ein korrekter, vollständiger Beweis ist. 00:18:16.841 --> 00:18:21.230 Und dann, damit schlägt man gleich sozusagen eine zweite Fliege tot, 00:18:21.230 --> 00:18:25.200 indem man dadurch eben auch die verfügbaren Bausteine vermehrt. 00:18:25.200 --> 00:18:29.190 Ja, also wenn man den ganzen Grundlagen mal formalisiert hat, 00:18:29.190 --> 00:18:32.558 dann hat man auch mit hoher Wahrscheinlichkeit schon ziemlich viel von dem, 00:18:32.558 --> 00:18:33.120 was so Standard ist. 00:18:33.120 --> 00:18:36.576 Standardmäßig in allen möglichen Forschungsbeweisen benutzt wird. 00:18:36.646 --> 00:18:39.551 Auch verifiziert natürlich nicht die neueren Dinge, 00:18:39.551 --> 00:18:42.457 aber halt die Grundlagen, die überall irgendwie benutzt werden. 00:18:42.457 --> 00:18:44.442 Die sind dann wenigstens schon mal vorhanden. 00:18:44.442 --> 00:18:45.485 Die kann man auch suchen. 00:18:45.485 --> 00:18:48.442 Man kann in dieser Datenbank tatsächlich nach Stichworten suchen, 00:18:49.034 --> 00:18:54.767 auch nach Sätzen suchen. Es ist alles nur so mäßig brauchbar. 00:18:54.767 --> 00:18:59.770 Ich habe da mal versucht, was einzugeben, aber man findet irgendwie wenig. 00:19:00.962 --> 00:19:04.550 Meine Vermutung ist, weil eben die Benennung nicht konsistent ist. 00:19:04.780 --> 00:19:07.012 Ja, ein Satz, der bei uns irgendwie so heißt, 00:19:07.523 --> 00:19:10.846 der heißt in einem anderen Kulturkreis irgendwie anders. 00:19:10.846 --> 00:19:13.488 Und schon in Frankreich haben die Sätze oft andere Namen, 00:19:13.488 --> 00:19:16.120