Die moderne Mathematik hat ein Problem: Sie ist nämlich zu kompliziert geworden. Selbst für Fachleute. Können Computer und KI die Zukunft der Mathematik sichern? Darüber sprechen wir heute hier im Spektrum Podcast. Mein Name ist Marc. Zimmer, schön, dass ihr dabei seid. Früher gab es hier noch die großen Universalgelehrten: Leonardo da Vinci, Isaac Newton oder Leibniz zum Beispiel. Die hatten von ganz vielen Naturwissenschaften Ahnung und meistens auch noch zusätzlich von Philosophie oder Theologie oder was weiß ich. Und heute ist das ganz anders. Viele Forschungsgebiete sind nämlich mittlerweile so speziell, dass teilweise weltweit nur noch ein Dutzend Menschen oder so daran arbeiten. Und besonders zu spüren bekommt das die Mathematik. Denn wo man erst mal auf 30 Seiten irgendwie einen Beweis verstehen muss, da ist es natürlich schwer, sich einfach mal reinzudenken, sogar wenn man selbst vom Fach ist. Und das ist natürlich ein Problem für den Fortbestand und das Weiterkommen in der Wissenschaft. Und hier sollen jetzt in Zukunft Computer eine immer tragendere Rolle einnehmen. Wie genau das aussieht und was eine Schülerin und ein Schüler aus Deutschland damit zu tun haben, darüber spreche ich jetzt mit Manon. Bischoff. Die ist Redakteurin für Mathe und Physik bei Spektrum der Wissenschaft und heute mein Gast hier im Podcast. Hallo Manon! Hi Marc! Ja. Manon, wir reden erst mal über ein ziemlich berühmtes Paradoxon. Das wurde überprüft, aber vielleicht sagen wir erst mal, um was geht es denn eigentlich? Was ist daran paradox? Also, es geht um das Banach Tarski-Paradoxon. Ich weiß nicht, ob du vorher schon mal davon gehört hattest. Nee, gar nicht. Ja, das wurde in den 1920er Jahren gefunden und das ist so in Mathekreisen sehr bekannt. Also man nimmt eine Kugel, zerlegt die in ganz viele Teile, also man sortiert die Punkte der Kugel um und am Ende, wenn man damit fertig ist, hat man zwei identische Kugeln, die genauso groß sind wie die erste. Also man hat die Kugel einfach verdoppelt. Okay, also das ist paradox, ja. Genau, ja. Das ärgert halt auch Mathematikerinnen und Mathematiker erst mal, weil wir kennen das ja überhaupt nicht aus der realen Welt, sage ich jetzt mal. Es ist nicht wirklich intuitiv und dafür verantwortlich für dieses Paradoxon ist eine Grundregel, sage ich jetzt mal, der Mathematik. Das werde ich später nochmal erklären, aber diese Grundregel heißt Auswahlaxiom und deswegen hatte man gedacht: Boah, vielleicht stimmt ja diese Grundregel nicht. Lassen wir die doch vielleicht einfach mal weg, dann haben wir dieses Banach-Tarski-Paradoxon nicht mehr. Hätte ich aber rausgestellt, danach wird alles nur noch schlimmer. Wenn man das weglässt, wird die Welt noch verrückter, die Mathewelt. Und deswegen hat man sich dann einfach damit abgefunden und gesagt: Ja gut, dann können wir halt eben Kugeln verdoppeln. Aber es beschreibt ja nicht wirklich die reale Welt, weil man muss wirklich einzelne Punkte, die nulldimensional sind, von dieser Kugel entfernen, also kleiner als jedes Atom, kleiner als jedes Teilchen. Und deswegen ist es aus rein physikalischer Sicht gar nicht möglich. Also es widerspricht dann insofern doch nicht mehr unserer Welt, weil in unserer Welt doch wahrscheinlich eher alles endlich ist. Da habe ich dich richtig verstanden. Das funktioniert mathematisch, aber es ist natürlich paradox, weil wir das in der richtigen Welt nicht erleben, dass wir eine Kugel zerlegen in Einzelteile und dann wieder daraus zwei Kugeln entstehen. Okay, jetzt hatte das lange Bestand. Du hast 1920er Jahre gesagt, also 100 Jahre hatte dieses Paradoxon Bestand. Und jetzt kommen ein Schüler und eine Schülerin ins Spiel und die haben es, man könnte fast sagen, gelöst. Vielleicht erstmal: Wer ist das denn? Was sind das für zwei? Also nur ganz kurz: Richtig gelöst haben sie es vielleicht nicht. Sie haben es sich genauer angeguckt und was Spannendes herausgefunden. Aber du sagst schon: eine Schülerin und ein Schüler, Chiara Cimino und Christian Krause heißen die. Und die haben eben an einem Jugendforschwettbewerb teilgenommen und haben sich dafür eine Aufgabe rausgesucht. Und sie wollten eben dieses Banach-Tarski-Paradoxon ein bisschen besser verstehen. Und die hatten dann auch so einen Mentor zugeschrieben bekommen und der hat sie auf eine Forschungsarbeit aufmerksam gemacht, die eigentlich lange vergessen wurde. Und zwar von einem französischen Forscher, und der hieß Olivier Leroy. Und der hat in den 90er Jahren sich auch dieses Banach- Tarski-Paradoxon richtig angeguckt und wollte es halt wirklich loswerden. Und ihm ist aufgefallen: Ich habe ja vorhin gesagt, man kann es umgehen, wenn man dieses Auswahlaxiom, heißt das, weglässt. Aber das macht dann alles noch schwieriger und irgendwie hat sich keiner so richtig damit zurechtgefunden. Und ihm ist aufgefallen, man kann auch mit Auswahlaxiom dieses Paradoxon, diese Verdopplung der Kugel umgehen. Und dafür muss man halt die Topologie ein bisschen ändern. Also das heißt, man greift wirklich in die abstrakte Mathematik rein, ändert da eine Kleinigkeit. Dadurch ändern sich verschiedene Definitionen und am Ende aber kann man halt keine Kugel mehr verdoppeln. So, um das jetzt einfach mal so zu sagen. Wie gesagt, er hat in den 90er Jahren daran geforscht. 1996 ist er gestorben und hat seine Ergebnisse nie veröffentlicht. Und deswegen haben Kollegen von ihm 17 Jahre später, also die haben alle seine Notizen zusammengesucht, haben das zusammengeschrieben und haben dann eine Arbeit im Jahr 2013 veröffentlicht. Die war aber jetzt halt auch französisch. Vielleicht eine schöne Sprache, aber ist jetzt nicht die Wissenschaftssprache, die irgendwie jeder beherrscht. Und deswegen war sie halt so gut wie vergessen, diese Arbeit. Und ja, Christian Krause und Chiara Cimino, die haben halt diese Arbeit untersucht. Ja, und wie haben sie das jetzt konkret gemacht? Also was sie gemacht haben, in ihrem Jugendforschprojekt, die Idee war: Wir nehmen einen Beweis und übersetzen den in ein Computerprogramm, damit das Computerprogramm dann prüfen kann, ob dieser Beweis wirklich stichhaltig ist. Und das haben sie gemacht. Also sie haben den Beweis von Leroy genommen, der da aufgeschrieben war, wo es auch keine Referenzen gab und es war kein richtiges Paper, wie man es sonst kennt, weil eben einfach nur seine Notizen zusammengefasst wurden auf Französisch. Das heißt, erst mal mussten sie sowieso das Französische verstehen. Dann mussten sie die Mathematik verstehen, die super abstrakt ist. Und dann haben sie die Lücken gefüllt, weil so mathematische Beweise, da steht oft so was drin wie: Ja, das kann man leicht zeigen oder der Schritt ist trivial und überspringt den einfach. Meistens ist es nicht trivial. Ja, und das haben die alles gemacht, haben die dann in verschiedene Teile zerstückelt und haben dann eben das Ganze in eine Computersprache, also in Computerprogrammiersprache übersetzt und dann in einen sogenannten Beweisprüfer eingegeben und konnten damit checken: Job, der Beweis stimmt. Es ist alles richtig. Okay. Beweisprüfer ist schon mal ein gutes Stichwort. Und ihr merkt auch schon, uns geht es ja gar nicht so sehr darum, dass ihr dieses Paradoxon irgendwie begreift, sondern das ist ein schönes Beispiel, was die beiden Schüler da gemacht haben für ein größeres Thema, über das wir heute sprechen wollen. Und da gehen wir vielleicht erst mal zum Grundproblem, Manon. Moderne Mathematik ist extrem schwer zu überprüfen, schreibst du bei Spektrum der Wissenschaft. Das war es ja wahrscheinlich schon immer. Also warum? Was ist das Problem? Ja, also ich glaube, das letzte oder vorletzte Mal, als wir miteinander gesprochen haben, da ging es um einen tausendseitigen Beweis. Ich erinnere mich. Ja, genau, tausend Seiten. Wow, okay. Und dann war das auch noch in einem Bereich, wo nur zwölf Leute überhaupt ein bisschen was checken. Und das ist mittlerweile gar nicht mehr so selten. Also die Mathematik ist super fragmentiert. Es ist halt echt so, dass wenn man eine Forschungsarbeit nimmt und nicht aus genau diesem Fachgebiet ist, also wenn jetzt jemand, der Algebraiker ist, sich eine Geometrieforschungsarbeit anguckt, dann wird er vielleicht nichts verstehen. Also das kann durchaus sein. Und also ich merke das an mir im Journalismus halt auch. Wenn ich jetzt Physikpaper nehme, dann klar verstehe ich auch nicht jedes Detail, aber ich verstehe zumindest so grob, was gemacht wurde, was die Idee dahinter war. Eigentlich relativ egal aus welchem Physikbereich jetzt, auch wenn das jetzt nicht mein Lieblingsthema ist. In der Mathematik ist es halt komplett anders. Also meistens bin ich halt wirklich einfach auf Fachleute angewiesen, die mir dann sagen hey, darum geht es, das ist die Idee, darum machen wir das. Und ja, das stimmt auch, was da steht. Also ich selbst bin da in den meisten Fällen halt einfach aufgeschmissen, leider. Ja, und das geht halt eben auch Fachleuten so. Also es ist halt nicht nur bei mir oder bei Journalisten, sondern es ist halt auch bei Mathematikerinnen und Mathematikern so. Ja, und da muss man vielleicht an der Stelle auch nochmal so ein bisschen, das habe ich auch beim Einlesen für mich gemerkt, für den Laien, der ich ja auch bin, erklären so Definitionen, Beweise, das ist eben wahnsinnig wichtig in der Mathematik. Ja, genau. Weil Mathe ist halt einfach nochmal was anderes als die anderen Naturwissenschaften. Also Physik, Biologie, Chemie, damit beschreibt man ja die Natur und man hat da so eine empirische Vorgehensweise. Also man macht Messungen und man versucht dann irgendwie mit einem Modell vielleicht die Natur zu beschreiben. Aber man wird halt niemals zeigen können, ob das Modell jetzt wirklich zu 100 Prozent stimmt oder nicht. Also man kann es ja immer nur abgleichen und solange es funktioniert, ist toll. Mathe ist da halt nochmal ganz, ganz, ganz anders. Also da setzt man was voraus, am besten irgendwie wenige, relativ einfache Grundregeln, Axiome, und darauf baut dann halt alles auf. Also in der modernen Mathematik von heute gibt es neun solche Axiome. Zu denen gehört auch das Auswahlaxiom, von dem ich vorhin gesprochen habe. Das sind ganz, wie gesagt, ganz einfache Grundregeln, so was wie Gesetze oder Gebote, wenn man so will. Die sagen dann so was aus, wie es gibt eine leere Menge. So, damit fängt man an und dann sagt man: Zweite Regel, man kann Mengen irgendwie vereinigen, also verbinden. Und von dort aus baut man dann halt alles irgendwie auf nach logischen Regeln, also nach Regeln wie: Wenn ich jetzt weiß, alle Menschen sind sterblich, alle Römer sind Menschen, dann folgt daraus, dass alle Römer sterblich sind. Also diese logischen Argumentationsketten. Und da merkt man halt schon, also man kämpft sich voran, so mit Definitionen, mit Sätzen. Das sind dann Aussagen, die man dann beweist anhand dieser Grundregeln. Das ist so die Idee dahinter. Und Mathematik ist eben nicht, wie man vielleicht in der Schule denkt, Rechnen, sondern das ist genau das einfach. Und genau das ist mit der Zeit halt immer komplexer geworden, sodass mittlerweile halt nicht mehr so viele Leute durchblicken. Ja, na klar, das wollte ich auch noch sagen. Also man kommt ja auch einfach immer weiter in der Wissenschaft und dadurch werden die Sachen aber natürlich auch komplizierter. Vielleicht auch der Grund, warum es nicht mehr diese, was ich vorhin meinte, Universalgelehrten gibt, weil einfach so viel Wissen in den einzelnen Disziplinen mittlerweile angehäuft wurde, dass man das ja gar nicht mehr alles checken kann, wahrscheinlich. Okay, also wir halten fest: Die moderne Mathematik hat ein Problem in dem Sinne. Und jetzt gibt es Hoffnung, nämlich durch Computer. Die sollen in Zukunft entscheidend helfen. Wie könnte das denn aussehen? Ja, also das Stichwort sind hier diese Beweisprüfer, von denen ich eben auch schon gesprochen habe. Und das ist eine Idee, die gibt es schon länger. Also seit den 50er, 60er Jahren gab es so die ersten Ansätze dafür. Und das Ganze nimmt aber jetzt erst Fahrt auf. Also die Idee ist, man nimmt eine Aussage, eine mathematische, so was wie 2 plus 2 ist gleich 4. Super easy. Und zerlegt die dann so weit, bis man sieht, wie die aus den Grundregeln folgt, also aus diesen Axiomen, auf denen die Mathematik aufbaut. Und man arbeitet sich so Schritt für Schritt immer weiter zurück, bis man sieht: Okay, jeder Schritt war korrekt. Und das prüft der Beweisprüfer. Also es ist ein Computerprogramm, das genau das macht. Und das klingt jetzt vielleicht erst mal einfach. Aber jetzt darfst du mal raten, wie viele Schritte es braucht, um von 2 plus 2 gleich 4 rückwärts zurück bis zu den Grundregeln der Mathematik zu kommen. Wie viele Schritte? Pfff, keine Ahnung. 10? Ja, ich hätte tatsächlich auch so in der Größenordnung gedacht. Also man muss erst mal definieren, was eine Zahl ist, was ein Plus ist, was ein Gleich ist. Wird schon irgendwie gehen. Es sind mehr als 26.000. Oha! Genau. Und jetzt wird auch das Problem klar, warum das mit den Beweisprüfern so lange gedauert hat, warum wir die jetzt noch nicht haben, dass die super easy funktionieren. Weil wenn man selbst für 2 plus 2 ist gleich 4 so viele Schritte braucht und der Computer eigentlich so viele Schritte machen müsste, um nachzugucken, dass das wirklich stimmt, ja keine Ahnung, braucht man halt ewig, um am Ende den Satz des Pythagoras zu zeigen oder irgendwas anderes. Ja, Wahnsinn. Okay, das heißt, habe ich jetzt durch den Artikel gelernt, man muss irgendwie auch gucken, wie kriegt man das in den Computer rein. Und da ist die Programmiersprache Lean, heißt die, ein sehr, sehr wichtiges Tool. Was hat es denn damit auf sich und was kann die? Also Lean ist relativ neu. Also die ist erst so um die 10 bis 12 Jahre alt als Programmiersprache. Und ich weiß nicht, kannst du programmieren oder hast du schon mal programmiert? Nee, nee, nee. Okay, also man hat ja immer so dieses Bild von so einem schwarzen Bildchen, wo so Zeilen drüber gehen. So sieht das dann natürlich dann halt auch aus. Aber ja, man definiert dort dann halt erstmal Größen, kann dann damit irgendwie rechnen. Also Lean baut eben auch auf den Grundregeln der Mathematik auf. Und um das jetzt sinnvoll nutzen zu können, also wenn ich jetzt wirklich damit zeigen will, 2 plus 2 ist gleich 4 oder was Komplexeres, was man ja in der Regel dann ja auch prüfen will, dann kann ich ja nicht immer wieder bei den Basics anfangen. Das heißt, man braucht so was wie Programmbibliotheken. Die gibt es auch in anderen Programmiersprachen für andere Sachen, um irgendwelche Prozesse halt einfach schneller abrufen zu können. In dem Fall ist es jetzt so, zum Beispiel in der Bibliothek kann so was eine Definition für eine Primzahl drin stehen. Da muss ich nämlich nicht jedes Mal definieren: Ja, eine Primzahl ist eine Zahl, die nur durch eins und sich selbst teilbar ist. Das weiß das Programm dann und dann kann ich damit rechnen. Und es arbeiten halt super viele Leute an dieser Mathebibliothek, die heißt Mathlib. Die hat auch mittlerweile fast zwei Millionen Zeilen Code, also nur um so mal den Umfang sich klarzumachen. Die wird halt von Freiwilligen erstellt. Es gibt Forscher, die angestellt sind in der Uni und dafür natürlich auch bezahlt werden, aber es gibt auch einige, die das halt einfach in ihrer Freizeit machen. Oder zum Beispiel eben auch Christian Krause und Chiara Cimino, die zwei, bei Jugend forscht mitgemacht haben. Die haben auch einen Teil ihres Projekts, was die da formalisiert haben, so nennt man diese Übersetzung in die Computersprache, ein Teil ihrer Arbeit ist dann in diese Mathlib reingeflossen, weil sie halt eben neue Sachen definiert haben oder grundlegende Größen halt eben in dieser Computersprache angelegt haben und jetzt auch andere darauf zugreifen können. Und früher gab es halt eben nur relativ wenige Freiwillige, die das gemacht haben, weil klar, das frisst halt super viel Zeit. In der Zeit forscht man ja auch nicht selbst an komplexen Fragestellungen oder so, sondern das ist natürlich auch super komplex und das ist auch eine Art von Forschung. Aber man generiert ja jetzt nicht neues Wissen über die Mathematik in erster Instanz, sondern man beschäftigt sich ja damit, dass man erstmal lauter bekanntes Wissen in diese Bibliothek rüberbringt. Erstmal vielleicht für einige langweilig, weswegen das auch nicht so viele machen wollten. Aber mittlerweile gibt es immer mehr Akzeptanz in der Community, weil es auch immer mehr Beispiele gibt, wie man halt eben diese Beweisprüfer nutzen kann, auch für moderne Beweise und für die moderne Mathematik und auch Fehler damit aufgedeckt wurden. Und man sieht das jetzt eben auch an den zwei Schülern, dass es halt immer bekannter wird. Und als ich mich mit den beiden unterhalten habe, haben sie halt auch gemeint, dass sie es so cool fanden, dass es so eine offene Community ist. Also man kann sich da austauschen. Sie kannten sich jetzt in der Mathe-Community noch nicht so sehr aus und irgendwann haben sie den einen Mathematiker, der ihnen da geholfen hat, mal gegoogelt und haben festgestellt, dass es halt so ein super namhafter Prof ist in der Community generell. Und der setzt sich halt und hilft dann Schülerinnen und Schülern. Also es ist sehr niedrigschwellig und nett. Das ist eine sehr, sehr schöne Geschichte. Ja, cool. Und auch Respekt an die beiden, auch dass man sich dann traut, da irgendwie als Schüler in so einer Community auch mitzumischen. Aber sehr, sehr cool. Also du hast gesagt: Formalisierung wird immer wichtiger. Und wenn man das Beispiel mit den beiden Schülern gehört hat, hast du vielleicht mal noch ein anderes Beispiel, woran wir sehen, dass da auch einiges passiert, gerade? Ja, genau. Ich bin für die Recherche nach Bonn gefahren. Das ist sowas wie die Mathe-Hauptstadt aktuell in Deutschland. Dort sind große Mathezentren und ein MPI und so. Und dort hat zum Beispiel ein Projekt stattgefunden, wie die Mathematik in Zukunft ablaufen könnte. Und das habe ich mir halt angesehen. Also kennst du die normale Vorgehensweise beim Publizieren von wissenschaftlichen Arbeiten? Da gibt es ganz viele Review-Prozesse und so weiter. Genau, ja. Also in der Mathematik wäre es so, man hat halt vielleicht einen Beweis zuerst gemacht und dann würde man es einem Gutachter geben oder man reicht es in einem Journal ein. Die geben das Gutachten weiter, die prüfen, ob alles richtig ist, ob es relevant ist und dann wird es publiziert. Und das könnte jetzt ganz anders aussehen durch die Beweisprüfer in der Mathematik. Und zwar, dass man halt erst seine Arbeit macht, so wie vorher auch. Also man fasst das zusammen, man hat einen Beweis. Dann formalisiert man den, also übersetzt den in Lean oder eine andere Programmiersprache. Dann lässt man es durch einen Beweisprüfer laufen, der dann sicherstellt, dass wirklich alles richtig gelaufen ist. Und da kann ich vielleicht auch nochmal betonen: Diese Beweisprüfer, das sind keine KI-Algorithmen oder so, sondern das sind ganz normale Algorithmen, die standardmäßig ablaufen. Das ist auch wichtig, weil die sollen ja eben keinen Fehler übersehen. Die sollen nicht halluzinieren oder so, sondern wirklich sicherstellen, da gibt es 100 Prozent keinen Fehler in diesem Beweis. Und wenn dann aber so ein Beweisprüfer gecheckt hat, die Arbeit ist richtig und man reicht es dann bei einem Journal ein, dann wissen die ja schon: Ja, saukool, das stimmt auf jeden Fall, was da steht. Also wir müssen das gar nicht mehr auf Richtigkeit prüfen. Jetzt brauchen wir nur noch zu schauen, ist es relevant genug, damit das bei uns irgendwie erscheint. Und das nimmt sowohl den Menschen Arbeit ab, die teilweise auch lästig und sehr langwierig ist. Auf der anderen Seite sorgt das halt aber auch dafür, dass keine fehlerhaften Sachen publiziert werden, was ja durchaus mal passiert. Weil du kannst dir ja vorstellen, wenn ein Beweis tausend Seiten lang ist, dann übersieht man ja auch gerne mal was. Und man kann sich halt nicht 100 Prozent sicher sein, dass alles stimmt. Und das ist auf jeden Fall schon mal sehr gut. Ein weiterer Punkt ist, dass dadurch, wenn man das formalisiert, schreibt man den Beweis ja meistens um. Und ich habe ja auch gesagt, man füllt alle Lücken. Und dadurch wird ein Beweis auch in der Regel verständlicher für Außenstehende. Und dadurch verstehen auch andere Mathematiker aus dem Bereich eher eine Forschungsarbeit und nicht eben nur die zwölf anderen Leute, die daran arbeiten. Also es macht an sich die Mathematik ein bisschen inklusiver. Das ist die Hoffnung. Ja, krass. Und das ist auf jeden Fall auch safe, dass dann die Computerprüfung ist auf jeden Fall sorgfältiger und besser als die menschliche Prüfung. Ja, deutlich. Auf jeden Fall. Und man geht halt wirklich davon aus, dass da gar keine Fehler stattfinden. Also es sei denn, es wäre jetzt irgendwo ein ganz schlimmer Programmierfehler, aber der wäre halt wahrscheinlich schon aufgefallen. Also deswegen kann man sich da eigentlich schon so wahrscheinlich wirklich 100 Prozent sicher sein in der Regel, dass es stimmt. Und in Bonn haben sie, ich habe ja gesagt, ich war dann dort, weil sie eben diese neue Vorgehensweise halt einfach mal testen wollten. Und das hat die Forschungsgruppe um Christoph Thiele, heißt er, die haben das in der Praxis getestet. Und die beschäftigen sich mit harmonischer Analysis. Das klingt nach Musik und das hat auch tatsächlich was damit zu tun. Aber so wie ich es verstanden habe, wenn man jetzt einen Ton oder so ein Instrument, so einen Klang macht, dann kann man diesen Klang in Obertöne zerlegen, die feste Frequenzen haben. Das Gleiche kann man mit Funktionen machen in der Mathematik. Also kannst du dir vorstellen, wenn du so eine Kurve hast, die eine Funktion beschreibt, dann kann man die in einfachere Bausteine zerlegen, die wie so Wellen sind mit einer bestimmten Frequenz. Und wenn man die Wellen richtig addiert, dann hat man am Ende diese komplizierte Form der Funktion raus. Das ist die Idee der harmonischen Analysis. Und das macht vieles sehr viel einfacher. Zum Beispiel kann man so auch Bilder komprimieren, weil man dann nur die Frequenzen speichern muss und nicht eine komplizierte Funktion als Ganzes. Auf jeden Fall sehr viel Anwendung, was in der Mathematik ja auch nicht immer der Fall ist. Und die Arbeitsgruppe von Christoph Thiele beschäftigt sich mit der Frage, für welche Funktionen ist das möglich, diese Zerlegung in diese einfacheren Frequenzbausteine. Weil für schöne, easy Funktionen, wie man die in der Schule kennenlernt, ist alles tiptop, da funktioniert das alles. Aber wenn die so richtig eklig werden, ist nicht mehr so klar. Und Thiele und seine Arbeitsgruppe, die haben einen Beweis dazu publiziert. Natürlich ein sehr abstraktes Problem. Und der Beweis ist relativ lang, also 30 Seiten. Und auch so, wie mir die Mathematiker gesagt haben, also das sagt nicht nur ich, ziemlich kompliziert. Und Floris van Dorn, das ist auch ein Mathematiker, der dort forscht, der sich mit Lean sehr gut auskennt, der hat gedacht, dieser Beweis ist ideal, um den mit Lean zu formalisieren. Weil es ist halt eben ein komplizierter Beweis. Das heißt, man hat einen Mehrwert davon, das wirklich zu machen. Da muss sich nicht ein Mensch damit rumschlagen, das wirklich prüfen. Und die einzelnen Methoden liegen schon Lean vor oder wird nicht so schwer zu sein, das zu formalisieren. Es ist machbar, sagen wir es so. Man wird nicht Jahre dafür brauchen. Ja, dann hat er sich da drangesetzt mit seinem Team und dann haben die das zusammen gemacht. Also dann wurden erst mal aus den 30 Seiten Beweis, ich habe ja schon gesagt, man muss dann immer ein bisschen nachfüttern, wurden 120 vierfache Länge. Und er hat das Ganze dann nochmal aufgespalten in 180 einzelne Teilbeweise, die dann zu prüfen waren. Und das alleine zu machen, ist dann schon wieder ziemlich aufwendig. Und deswegen hat er so eine Online-Plattform genutzt, wo ganz viele Lean-Fans oder Begeisterte halt sind. Und hat 20 Freiwillige gefunden, die sich an dem Projekt beteiligt haben. Und haben die das auch geschafft. Also das ist relativ kurz. Vor ein paar Jahren hat so ein Beweis noch zehn Jahre teilweise gedauert zum Formalisieren. Vor mehr als zehn Jahren, weil es muss ja zehn Jahre gedauert haben. Und jetzt wissen sie, der Beweis von der Arbeitsgruppe um Thiele der ist korrekt. Jeder Zwischenschritt, der dabei gemacht wurde, ist korrekt. Und ja, jetzt können die das einfach bei einem Journal einreichen. Und die wissen das auf jeden Fall. Das müsste jetzt nicht nochmal geprüft werden. Und das könnte halt jetzt in Zukunft einfach gang und gäbe werden. Und wie ich ja schon erwähnt habe, das Gute ist, es werden alte Arbeiten vor allem momentan formalisiert. Und da wurden auch schon Fehler gefunden, die dann korrigiert werden mussten. Also, es hat schon seinen Sinn. Ja, voll spannend! Da tut sich richtig was. Und man hört es auch bei dir so ein bisschen raus. Die Hoffnungen sind natürlich groß, aber du hast auch schon beschrieben, es ist jetzt nicht alles so ganz einfach, trotzdem dabei, auch wenn die Ergebnisse gut sind. Also, welche Herausforderungen gibt es denn noch bei der Formalisierung? Also, wie gesagt, das ist super aufwendig. Floris Van Dorn meinte, dass man für einen einseitigen Beweis aus dem Lehrbuch, den man jetzt irgendwie vielleicht im Bachelorstudium so bekommt, wo auch alle Definitionen schon in Lean bereitstehen, mehrere Wochen Arbeit reinstecken muss, bis der dann halt formalisiert ist. Also schon, ja, man muss motiviert sein. Und ich habe mir das auch mal vorführen lassen, als ich da vor Ort war. Für ein einfaches Beispiel: Es kommt ein Satz, und der sagt, dass es unendlich viele Primzahlen gibt. Weiß man vielleicht auch aus der Schule, hat man schon mal gehört. Genau. Und Primzahlen, wie gesagt, das sind Zahlen, die nur durch eins und sich selbst teilbar sind, also keine anderen Teile haben. Und der Beweis dafür, den hat Euclid vor, ich glaube, 2300 Jahren oder so, sich überlegt. Den kann man auch relativ einfach noch erklären. Also, man nimmt erst mal an, es gäbe nur endlich viele Primzahlen, und dann führt man das Ganze auf einen Widerspruch. Also, man führt es auf eine falsche Aussage. Dann weiß man, okay, da muss das Gegenteil richtig sein. Also, es muss dann demnach unendlich viele geben. Und man sagt, okay, wir gehen davon aus, es gäbe wirklich nur endlich viele Primzahlen. Und jetzt sei die größte Primzahl, meinetwegen, n. Und wenn ich jetzt das Produkt von allen Zahlen von 1 bis n bilde und dann plus 1 rechne, habe ich eine neue Zahl, und die ist durch keine der vorherigen Zahlen teilbar. Sie muss nach der Definition wieder eine Primzahl sein, aber sie ist größer als n. n war ja die größte, deswegen muss es unendlich viele geben. Genau. Und ich habe mir angeguckt, wie er diesen Satz, der sich relativ easy noch erklären lässt, in Lean eingibt. Also, das Computerprogramm heißt so, und die Sprache heißt so. Das ist ein bisschen verwirrend. Also, in diesem Beweisprüfer. Und das war erst mal nicht ganz so einfach. Zum Glück war schon viel in dieser Bibliothek da, aber dann hat er eine Fehlermeldung auf einmal mittendrin zurückbekommen. Und zwar, weil das Programm nicht prüfen konnte, ob 4 ungleich 0 ist. Ja, und ich dachte halt auch so, what the fuck. Also, Lean kann wirklich so auch von alleine kleine Beweise führen, aber festzustellen, dass 4 nicht gleich 0 ist, das muss man ihm nochmal extra sagen. Also, das ist komplett verrückt irgendwie. Oder sieht man halt, okay, also da gibt’s noch Verbesserungspotenzial bei dem ganzen Ding. Aber wie gesagt, es arbeiten mittlerweile immer mehr Leute daran, und die bearbeiten auch die Programmversion, und dadurch wird es auch immer besser. Und die hoffen ja auch, das immer handlicher zu machen, sodass auch immer mehr Leute auch Bock bekommen, damit zu arbeiten. Es gibt jetzt auch eine Uni- Kurse dafür. Das gab es zu meiner Zeit zum Beispiel noch gar nicht, also zumindest nicht an meinen Unis. Und dann gibt’s jetzt auch noch Geld von außerhalb. Also, es gibt einen Milliardär, der Alex Gerko, der hat 10 Millionen Dollar investiert, damit Lean besser gemacht wird. Und auch in den USA, was ich ganz interessant fand, obwohl die ja total auf Sparkurs gerade sind und viele Forschungsprojekte ja beenden, hat die National Science Foundation jetzt bekannt gegeben, dass sie mehrere Projekte mit Lean fördert. Also, man sieht schon, da wird überall Potenzial gesehen. Ja, krass! Auch sehr, sehr spannend, was da in Zukunft noch passiert. Und Manon, ich würde gerne zum Abschluss noch kurz fragen: Du hast vorhin einmal gesagt, dass wir da eben nicht über KI-Algorithmen sprechen, sondern über ganz in Anführungszeichen normale. Da wir uns aber ja auch oft hier im Podcast über KI unterhalten, nochmal die Frage zum Abschluss: Auch KI wird ja in Zukunft wahrscheinlich da immer eine wichtige Rolle spielen, auch bei der Mathematik und ihrer Zukunftsfähigkeit, oder? Ja, total! Also, die ist da auch so ein großer Hoffnungsträger, weil dieses Formalisieren, was ja gerade so viel Zeit frisst, ist ja wie eine Art Übersetzung. Und ich meine, wir benutzen ja alle DeepL oder JGPT oder so zum Übersetzen auch und merken, was das für ein Potenzial hat. Und das verstehen ja natürlich auch die Entwickler, die KI-Entwickler, und versuchen, Sprachmodellen halt auch eben diese Übersetzung von „Ich habe hier eine Aussage, eine mathematische mit Formeln und mit geschriebener Sprache“ auch, also Beweise enthalten, auch ganz normale Argumentationen in englischer Sprache zum Beispiel. Und dass man genau das packt und in Lean formalisiert, zum Beispiel, oder in der anderen Programmiersprache. Da wird schon dran gearbeitet. Es gibt auch ein paar Prototypen, die funktionieren wohl, aber alle noch nicht so gut, haben mir die Mathematiker gesagt. Also, die arbeiten noch nicht damit, hoffen aber auch und sagen ja auch, das Feld verändert sich so schnell, es wird wahrscheinlich nicht mehr lange dauern. Und die freuen sich auch schon drauf. Was auch noch eine andere spannende Perspektive ist, aus meiner Sicht, ist, wenn man so ein großes Sprachmodell einfach random irgendwelche Matheinhalte generieren lässt. Also, man könnte ja JGPT sagen: „Hier, denkt ihr mal so ein paar Sachen aus.“ Und da wird natürlich viel Mist dabei sein, aber man kann das ja alles automatisiert prüfen über einen Beweisprüfer. Und vielleicht sind da ja auch richtige Sachen dabei, und das könnte man dann halt direkt prüfen lassen und hat dann direkt vielleicht auch ein paar wahre Aussagen und vielleicht ein paar neue Erkenntnisse. Also, das sind so ein bisschen Gedanken, die es gibt, was so alles in Zukunft machbar sein könnte. Ja, und so wird vielleicht das Problem, das wir eingangs beschrieben haben, nämlich dass die Mathematik, du hast es schön ausgedrückt, sehr fragmentiert ist, doch mittlerweile. Und viele Teilsdisziplinen gar nicht wieder Ahnung davon haben, was die anderen so machen. Vielleicht in Zukunft ein bisschen gelöst durch Computer und eben auch KI. Manon hat sich das angeschaut für Spektrum de. Da findet ihr auch den Text dazu, wenn ihr nochmal nachlesen wollt, und auch den Text über die Schülerin und den Schüler, die diesen Beweis dann nochmal überprüft haben. Und Manon, dir sag ich vielen vielen Dank fürs Erklären. Ja, danke für die Einladung! Und auch euch vielen, vielen Dank, dass ihr zugehört habt bei dieser Folge vom Spektrum Podcast. Eine neue gibt es dann wie immer kommenden Freitag. Seid auch gern dann wieder dabei. Abonniert den Podcast, wenn ihr keine Folge mehr verpassen wollt. Mein Name ist Max Zimmer, und ich sag Tschüss und macht’s gut. Spektrum der Wissenschaft. Der Podcast von detektor.fm.
