Terence Tao über Proof-Checker und KI-Mathe-Copiloten
(scientificamerican.com)- Da mathematische Beweise immer strenger formalisiert werden, verändern Tools wie Lean die Art, wie menschliche Beweise verifiziert werden, und die Vertrauensbasis großer Kooperationen
- Mit dem Aufbau von Standardbibliotheken wie mathlib sinkt die Einstiegshürde, um von Sätzen auf Bachelor-Niveau bis hin zu neuen Fachgebieten zu formalisieren
- Bei der Formalisierung der PFR-Vermutung übernahmen mehr als 20 Beteiligte kleine Beweisschritte; Terence Tao konzentrierte sich eher auf die Steuerung der Gesamtrichtung als auf eine zeilenweise Prüfung
- KI wird Mathematik vorerst weniger „lösen“, sondern eher als Proof-Copilot bei Formalisierung, Verifikation und repetitiven Aufgaben helfen
- Mathematische Forschung könnte sich zu expliziteren und stärker arbeitsteiligen Aufgaben wandeln, etwa menschliche Richtungsentscheidungen, detaillierte Formalisierung, KI-Training und Interpretation von KI-Beweisen
Wie Formalisierung mathematische Zusammenarbeit verändert
- Traditionelle mathematische Forschung ähnelte eher kleinen Kooperationen; Tao sieht normalerweise etwa 5 Personen als ungefähre Obergrenze für die Größe einer Zusammenarbeit
- Mit automatischen Proof-Checkern kann man auch mit Hunderten von Menschen zusammenarbeiten, die einander nicht kennen
- Beitragende laden Code hoch, und der Lean compiler verifiziert ihn
- Vertrauen muss nicht nur auf persönlichen Beziehungen beruhen, sondern kann durch Ergebnisse formaler Verifikation bestätigt werden
- Bei der Formalisierung des jüngsten Ergebnisses zur Polynomial-Freiman-Ruzsa(PFR)-Vermutung waren mehr als 20 Personen beteiligt
- Der Beweis wurde in viele kleine Schritte aufgeteilt
- Jede beteiligte Person übernahm den Beweis eines Schritts
- Tao verwaltete eher die Gesamtrichtung des Fortschritts, statt jeden Beitrag Zeile für Zeile zu prüfen
Nicht alle Mathematiker müssen Programmierer sein
- In Formalisierungsprojekten ist Arbeitsteilung möglich
- Manche konzentrieren sich auf die mathematische Richtung
- Andere spezialisieren sich darauf, kleine mathematische Bausteine in formale Beweise zu übersetzen
- Auch Mathematiker, die wie Peter Scholze nicht besonders computererfahren sind, können an Lean-Projekten teilnehmen
- Wenn große mathematische Aufgaben in kleine Teile zerlegt werden, kann man zu bestimmten Teilaufgaben beitragen, ohne die gesamte Theorie zu verstehen
Lean, mathlib und Suche machen es praktikabel
- Einer der wichtigsten Gründe, warum formale Mathematik praktikabel geworden ist, ist die Weiterentwicklung standardisierter Mathematikbibliotheken
- In Lean gibt es ein großes Projekt namens mathlib
- Grundlegende Sätze der Bachelor-Mathematik wie Analysis und Topologie werden nach und nach in die Bibliothek aufgenommen
- Ziel ist es, die Bibliothek bis auf Graduiertenniveau auszubauen
- Dadurch wird es leichter, neue mathematische Gebiete zu formalisieren
- Um Beweise zu erstellen, muss man bereits als wahr bestätigte Sätze finden; deshalb werden auch intelligentere Suchmaschinen wichtiger
- Nachdem das gesamte PFR-Projekt formalisiert war, dauerte die Verifikation per Kompilierung nur etwa 30 Minuten
- Der Engpass liegt weniger bei Rechenleistung als bei Bedienbarkeit, Benutzerfreundlichkeit und der Anpassung der Menschen an die Tools
- Lean gilt derzeit als formale Sprache mit der aktivsten Community
- Für Projekte einzelner Autoren können andere Sprachen besser geeignet sein
- Lean ist leicht zu lernen und hat gute Bibliotheken sowie eine starke Community
- Es könnte später durch Alternativen ersetzt werden, ist derzeit aber die dominierende formale Sprache
Noch hohe Kosten der Formalisierung
- Tao meint, er könne ein bestimmtes Projekt zwar formalisieren, müsste dafür derzeit aber möglicherweise einen Monat seiner Zeit investieren
- Noch ist nicht der Punkt erreicht, an dem alle Ergebnisse routinemäßig formalisiert werden
- Wenn es beim Lernen von Lean hilft
- Wenn großes Interesse an der Korrektheit eines Ergebnisses besteht
- Man sollte Projekte auswählen, bei denen Formalisierung echten Wert liefert
- Mit besserer Technologie können die Kosten der Formalisierung sinken
- Derzeit kann sie zehnmal länger dauern als der herkömmliche Weg
- Künftig könnte das auf etwa das Doppelte und weiter sogar auf weniger als den einfachen Aufwand sinken
KI kann zum Copiloten von Mathematikern werden
- Tao stellt sich vor, dass Mathematiker künftig Beweise nicht direkt eintippen, sondern sie Systemen wie GPT erklären, während die KI laufend eine Lean-Formalisierung versucht
- Wenn die Verifikation erfolgreich ist, könnte man zugleich einen LaTeX-Artikel und einen Lean-Beweis bereitstellen
- Wenn Nutzer es wünschen, könnte daraus ein Assistent werden, der bis zur Einreichung bei einem Journal hilft
- Der derzeit schnellste Weg zur Formalisierung besteht weiterhin darin, dass Menschen zuerst die Idee und einen Entwurf des Beweises erstellen
- Langfristig könnten auch Projekte möglich werden, in denen Menschen kleine Teile formalisieren, ohne den gesamten Beweis zu kennen, und KI und Menschen diese gemeinsam verbinden, um einen großen Satz zu beweisen
- Tao meint, dass es mehrere Jahre dauern wird, bis ein solcher Ansatz möglich wird
- Die heutige Technologie reicht noch nicht aus, und Formalisierung ist weiterhin eine mühsame Arbeit
Abstand zur Prognose, dass „Mathematik gelöst“ wird
- Tony Wu und Christian Szegedy haben gesagt, Mathematik werde innerhalb von 2 bis 3 Jahren in dem Sinne „gelöst“ sein, dass Maschinen Beweise besser finden als Menschen
- Tao hält es für möglich, dass KI innerhalb von 3 Jahren für Mathematiker nützlich wird und es deutliche Fortschritte gibt, sieht Mathematik aber nicht als gelöst an
- KI kann zu einem Copiloten werden, den man um Hilfe bittet, wenn ein Schritt in einem Beweis wahr zu sein scheint, Menschen ihn aber nicht sofort erkennen
- Selbst wenn KI Mathematik auf dem heutigen Niveau von Menschen betreibt, können menschliche Mathematiker zu höherer Mathematik weitergehen
- Durch KI könnte es auch möglich werden, auf einmal Hunderte oder Tausende von Sätzen zu beweisen
- Menschliche Mathematiker übernehmen dann die Rolle, zu dirigieren, was die KI tun soll
- Tao hält einen Zeitplan von 2 bis 3 Jahren für diese Veränderung für etwas aggressiv
Beweisverständnis und KI-generierte Beweise
- Ein mathematischer Beweis ist nicht nur ein Verfahren zur Überprüfung von Wahrheit, sondern auch ein Prozess des Verstehens, warum etwas wahr ist
- In naher Zukunft wird KI vermutlich zuerst langweilige und triviale Arbeiten automatisieren, während Menschen weiterhin die Richtung vorgeben
- Wenn KI schwer verständliche und unschöne Beweise liefert, können Menschen diese Beweise erneut analysieren
- Zum Beispiel lässt sich bei einem Beweis, der aus 10 Annahmen eine Schlussfolgerung gewinnt, prüfen, ob er auch ohne eine der Annahmen gilt
- Es könnte eine neue Art von Mathematikern entstehen, die aus KI-generierten Beweisen Einsichten extrahieren
- Frühe KI-Beweise könnten zunächst einsichtslos wirken
- Menschen können diese Beweise verständlicher machen und ihre Struktur herausarbeiten
Ungelöste Probleme und Grenzen der KI
- Um unbewiesene Vermutungen zu beweisen, muss man sie zuerst in kleinere Teile zerlegen
- Es ist viel leichter, ein Problem in ein schwierigeres Problem zu verwandeln, als in ein leichteres
- Tao meint, KI habe noch nicht gezeigt, dass sie bei dieser Zerlegungsarbeit besser ist als Menschen
- Interessant ist der Einsatz von KI, um mögliche Verbindungen zwischen verschiedenen Gebieten vorzuschlagen
- Derzeit ist die Erfolgsquote niedrig
- Von 10 Vorschlägen könnte nur einer interessant und 9 nutzlos sein
- Tao glaubt, dass sich das künftig ändern könnte
Das Datenproblem mathematischen Wissens
- Eines der Probleme beim Training mathematischer KI ist, dass es nicht genügend Daten gibt
- Online-Artikel lassen sich für das Training nutzen, aber viel mathematische Intuition steckt nicht in Artikeln
- Gespräche zwischen Mathematikern
- Vorlesungen
- Die Art, wie Studierende betreut werden
- Fehlgeschlagene Versuche und Korrekturprozesse
- Veröffentlichte Beweise sind komprimierte Ergebnisse, und Menschen veröffentlichen tendenziell nur Erfolgsgeschichten
- Wirklich wertvolle Daten sind Prozesse, in denen etwas versucht wurde, nicht gut funktioniert hat und anschließend korrigiert wurde
- In Zukunft könnten Forschungsversuche und Fehlschläge aufgezeichnet und für KI-Training oder zur Vermeidung wiederholter Fehlschläge durch andere Forschende genutzt werden
- Tao nennt als Beispiel eine Situation, in der man der Aufzeichnung des Forschungsprozesses zustimmt, um ein fortgeschrittenes System wie AI Lean im Jahr 2040 zu nutzen
Wandel hin zu expliziterer Mathematik
- Viel mathematisches Wissen ist in den Köpfen einzelner Mathematiker eingeschlossen, und nur ein winziger Teil bleibt explizit erhalten
- Je mehr formalisiert wird, desto mehr implizites Wissen wird zu explizitem Wissen
- Formalisierte Lehrbücher können zu interaktiven Lehrbüchern führen
- Sie beginnen mit einer hochrangigen Erklärung eines Beweises
- Unverständliche Schritte lassen sich detaillierter aufklappen
- Falls gewünscht, kann man bis auf die Ebene der Axiome hinabgehen
- Ein solcher Ansatz kann es Mathematikern aus einem Gebiet erleichtern, zu einem anderen Gebiet beizutragen
- Teilaufgaben großer Projekte können präzise festgelegt werden
- Man kann an den nötigen Bausteinen mitarbeiten, ohne das Ganze zu verstehen
1 Kommentare
Hacker-News-Kommentare
https://archive.is/Idouw
Der Ausdruck project manager mathematicians erinnert an Edsger Dijkstras satirischen Text „A letter to my old friend Jonathan“ [1] von 1975 und den Folgebeitrag [2].
Darin zeigte und kritisierte er, wie lächerlich es wäre, wenn die Art, Software zu entwickeln, auf die Mathematik angewandt würde; in gewisser Weise war das aber vorausschauend.
Kernpunkt war die Kritik an der Absurdität, geistige Eigentumsrechte, insbesondere auf mathematische Wahrheit, anzuwenden. Glücklicherweise scheint dieser Teil in der heutigen Entwicklung hin zur Mechanisierung kein großes Problem zu sein.
[1]: https://www.cs.utexas.edu/users/EWD/transcriptions/EWD04xx/E...
[2]: https://www.cs.utexas.edu/users/EWD/transcriptions/EWD05xx/E...
Ein aufschlussreicher Text, aber was darin fehlt, ist meiner Ansicht nach der Punkt, dass LLMs zunehmend auf übermenschliche Weise abstrahieren.
Tao sagte: „Es ist leicht, ein Problem schwerer zu machen, aber schwer, es einfacher zu machen, und AI hat nie gezeigt, dass sie darin besser ist als Menschen.“ Doch aufgrund der Funktionsweise von LLMs könnten deutlich höhere Ebenen von Einsicht möglich werden.
Derzeit sind sie eher Helfer, Faktenprüfer und Erlediger langweiliger Arbeit, aber bald werden sie Instanzen sein, die Einsichten vorschlagen. Schon heute komprimieren LLMs Embeddings und Wissen und verfügen über Einsichten, die wir nicht sehen.
Die Szene, in der Hinton den Zusammenhang zwischen einer Atombombe und einem Komposthaufen als Beispiel anführt: https://www.youtube.com/watch?v=Gg-w_n9NJIE&t=4613s
Es sind lediglich Maschinen, die darauf trainiert wurden, die Art nachzuahmen, wie Menschen schreiben, und es gibt keine Trainingsdaten, die nötig wären, um etwas Klügeres als Menschen nachzuahmen.
Ich habe keinen Zweifel daran, dass Machine Learning die menschliche Intelligenz übertreffen wird, aber der Engpass besteht darin, einen Weg zu finden, wie es statt einer Regression über alle Texte der Welt ohne menschliches Eingreifen aus seinen eigenen Outputs lernen kann.
Ramanujan machte ohne reguläre Ausbildung und mit nur wenigen Mathematikbüchern glänzende mathematische Entdeckungen; aus Sicht der Trainingsdaten eines Machine-Learning-Modells ist das eine verschwindend geringe Menge.
Es dauerte etwa 10 Sekunden, das in Worte zu fassen, aber wenn man die nötigen Informationen kennt, ist die Antwort offensichtlich.
Hinton sagt, dies zeige analoges Denken, aber es gibt online viele Gartentexte und physikalische Erklärungen zu Komposthaufen, und es ist gut möglich, dass ChatGPT sie schon im Training gesehen hat.
Deshalb wirkt dieses Beispiel wie ein Fall, in dem nicht kontrolliert wurde, ob das LLM die Antwort in den Trainingstexten praktisch bereits gesehen hatte.
Interessant ist auch die Stelle später im Video, in der Ilya sagt: „Es gibt einen Existenzbeweis. Das menschliche Gehirn ist ein neuronales Netz“ (https://youtu.be/Gg-w_n9NJIE?t=4966). Ich stimme der Position, dass auch das menschliche Gehirn ein neuronales Netz ist, im Großen und Ganzen zu, sehe aber auch eine philosophische Weggabelung, weil es viele Gegenargumente gibt: Echte Neuronen arbeiten nicht mit 8 Bit, und Zelltypen, DNA sowie das hormonell-chemische Umfeld unterscheiden sich.
Das ist innerhalb von Minuten bis Stunden möglich.
Um dagegen einen weiteren menschlichen Experten zu bekommen, muss jemand auftauchen, der Mathematik als Beruf mag, jahrzehntelange Ausbildung und fortgeschrittene Spezialisierung durchlaufen, und es gibt keine Garantie, dass diese Person bis zum Ende durchhält und ein Niveau erreicht, auf dem sie die Wissensfront voranschieben kann.
Während man auf diese Zeit wartet, könnte man auch Billionen parallel arbeitender AI-Experten schaffen.
Die Bandbreite, mit der das menschliche Gehirn neue Informationen aufnimmt, ist gering; Maschinen dagegen können Lebenswissen in Sekunden replizieren, Tausende Gespräche parallel führen und sogar Teile eines Gehirns serialisieren und an andere AIs schicken. Wenn wir erst programmierbare Materie erreichen, könnte man exponentiell Computronium erzeugen und so etwas wie einen Omega-Punkt ermöglichen, bei dem Tausende Jahre Forschung in Sekunden erledigt werden.
Ich verstehe von Mathematik überhaupt nichts, musste aber an die Geschichte der Software denken. Früher waren erstaunliche Projekte wie RollerCoaster Tycoon Werke, die fast von einer einzigen Person geschaffen wurden.
Danach wurde Software Engineering auf eine Weise modularisiert, die dem in dem Interview Beschriebenen ähnelt, und heute ist daraus eine riesige Montagelinie geworden, in der Leute wie ich beruflich React ausspucken; die Produktivität pro Person oder das erforderliche Können scheinen gegen nahezu 0 zu gehen.
Ich habe den Eindruck, dass in der Blütezeit eines Fachgebiets ein Genie hundert Dinge im Kopf behalten und herausragende Arbeit leisten kann, und dass dieses Gebiet, sobald es durch eine Montagelinie ersetzt wird, nichts wirklich Wertvolles mehr hervorbringt.
Software Engineering hat nicht aufgehört, großartige Dinge zu tun; ich sehe eher das Gegenteil.
Spaß beiseite: Irgendwann kommt der Moment, in dem man einen kritischen Bug beheben muss, und dann zeigt sich das Können. Nur weil ein Produkt oder Service stabil und profitabel geworden ist, heißt das nicht, dass die ursprünglichen Entwickler weg sind oder dass niemand mehr Großes leisten kann.
Die Aussage, dieses Feld bringe nichts wirklich Wertvolles mehr hervor, ist sehr falsch.
Es fühlt sich an, als würde man eine Kathedrale, die 100 Menschen über 100 Jahre gebaut haben, mit einer Hütte vergleichen, die eine Person in einem Monat errichtet hat. Die Hütte steht auch und bietet Wohnraum, aber sie ist keine Kathedrale.
Im Web Development ist es schon schwer, nur bei Python mitzuhalten, weil es für jedes kleine Zahnrad im Getriebe so viele Frameworks und Technologien gibt.
Können folgt im Allgemeinen einer Lognormalverteilung, daher gibt es naturgemäß nur wenige Ausnahmetalente; und in einem frühen, kleinen Feld kann wegen fehlender Unterstützungsinfrastruktur nur überleben, wer extremes Talent hat, wodurch die Dichte an Spitzenkräften unrealistisch hoch werden kann.
Eine To-do-Listen-App mit 47 aktuellen Frameworks krampfhaft zusammenzustöpseln und bedeutende Wirkung zu erzielen, sind grundlegend verschiedene Dinge.
Aus Kosten-Nutzen-Sicht gibt es ein starkes lokales Optimum darin, billig viel Code auszustoßen, statt langfristig in große Dinge zu investieren; je reifer ein Feld wird, desto niedriger wird die Kompetenzuntergrenze, um diesen Punkt zu erreichen.
Es gibt auch nicht viele Organisationen, die sich darauf konzentrieren, Spitzentalente auszubilden. Deshalb lässt sich leicht erklären, warum mit dem Wachstum eines Feldes das durchschnittliche Können im unbeaufsichtigten Zustand sinkt; und wenn man die Verteilung falsch behandelt, kann es später teuer werden, das zu korrigieren.
Computerverifizierte Beweise sind ein Bereich, in dem KI in ziemlich naher Zukunft nützlich werden könnte. Allerdings vielleicht eher wie das neuronale Netz einer Schach-Engine als wie ein vollständiges LLM.
Alles von Hand zu beweisen ist langweilig und zeitaufwendig, daher werden bereits viele Solver genutzt, aber Taktiken oder Solver tun sich schwer, wenn man ihnen zu viele Sätze und Hilfssätze hinwirft.
Ein neuronales Netz als Suchmaschine, die relevante Hilfssätze per Pattern Matching findet, passt gut dazu.
Induktion und Unifikation höherer Ordnung sind im Grunde ebenfalls Code-Synthese, und es ist sehr ineffizient, alle möglichen Syntaxbäume blind durchzuprobieren.
Solver machen ohnehin Backtracking, daher ist es in Ordnung, wenn die KI zu 95 % nutzlose Hilfssätze liefert, und es könnte dramatisch besser sein als manuelle Suche.
Allerdings bin ich mir nicht sicher, ob computerverifizierte Beweise für die Kommunikation zwangsläufig gut sind. Von Menschen gelesene Beweise sind nicht nur wegen ihrer Länge auf hoher Ebene und lassen Details aus, sondern aus mehreren Gründen.
Das Kernproblem ist, dass sie mit den formalen Definitionen der mathematischen Objekte verbunden sein müssen, die im Beweis verwendet werden.
Menschen denken aber nicht so, wenn sie Beweise schreiben oder lesen. Normalerweise hat man ein hochgradiges, informelles Gefühl dafür, was man „moralisch“ tut, und füllt die formalen Details nach Bedarf aus.
Bei Computercode liegt die formale Semantik der Sprache dem mentalen Modell viel näher, deshalb funktioniert das bis zu einem gewissen Grad; in der Mathematik ist das Ziel im Allgemeinen ein anderes.
Die sledgehammer-Strategie von Isabelle kombiniert automatische Theorembeweiser wie E, Z3, SPASS und Vampire, um zu versuchen, ein Ziel zu beweisen oder zu widerlegen.
In der Theorie sieht das okay aus, aber in der Praxis bekommt man rekonstruierte Beweise, die ein Dutzend scheinbar beliebiger Hilfssätze anwenden; solche Beweise sind unlesbar und sehr fragil.
Es sieht nicht so aus, als würde KI dieses Problem auf magische Weise lösen.
Aktuelle neuronale Netze sind extrem sample-ineffizient, und Datensätze für formale Mathematik sind viel kleiner als Datensätze wie Python-Code.
Terence Tao hat vor ein paar Monaten einen hervorragenden Vortrag zu diesem Thema gehalten und geht dabei ausführlicher auf die Nutzung von Lean ein: https://www.youtube.com/watch?v=AayZuuDDKP0
Ein praktizierender Mathematiker soll während seiner Forschung GPT-4o dazu gebracht haben, ein vermutlich neues Lemma zu beweisen
„Mein Partner ist Mathematiker und hat letzte Woche zum ersten Mal ChatGPT genutzt, um ein paar Lemmata für seine Forschung zu beweisen. Er vermutete bereits, dass diese Sätze wahr sind, und hatte auch grob einen Ansatz, war aber kein Experte für Aussagen dieser Art. Es war das erste Mal, dass er vom Modell einen korrekten und nützlichen Beweis bekommen hat
Das erste Lemma hatte ein Mitarbeiter bei Berechnungen für kleine e-Werte entdeckt. ChatGPT fand den Beweis nicht, bevor man ihm sagte, es solle die Möbius-Funktion ausprobieren
https://chatgpt.com/share/9ee33e31-7cec-4847-92e4-eebb48d4ff...
Das zweite wirkt etwas standardmäßiger und hätte wohl auch Mathematica hinbekommen. Aber Mathematica liefert keine saubere Herleitung, daher ist es trotzdem nützlich
https://chatgpt.com/share/7335f11d-f7c0-4093-a761-1090a21579...“
Solche Dinge werden bei Schlussfolgerungen und anspruchsvollen Themen beängstigend gut
Wenn sich das Machine-Learning-Feld weiter darauf konzentriert, LLMs zusätzlich zu ihrem weitgehend System-1-Denken um System-2-Fähigkeiten zu ergänzen, dürfte es turbulent werden
Beeindruckendes Gedächtnis, kein neues Schlussfolgern
Wir haben es nicht als Summe über Partitionen mit |τ|!-Koeffizienten betrachtet, sondern als Summe über geordnete Partitionen; beides ist natürlich dasselbe
Wenn man zyklisch geordnete Partitionen nimmt, also Koeffizienten (|τ|-1)! statt |τ|!, erhält man 0 statt (-1)^e
Berens kombinatorischer Beweis wählt ein besonderes Element aus und konstruiert eine Bijektion zwischen zyklisch geordneten Partitionen gerader und ungerader Länge, indem dieses Element, falls es allein steht, mit dem nächsten Block zusammengelegt wird, andernfalls in einen eigenen Block abgespalten wird
Im Fall einer linearen Ordnung wendet man dasselbe vom letzten Element aus an; Partitionen, bei denen das letzte Element im letzten Block allein steht, werden jedoch nicht gematcht, daher geht man rekursiv zum nächsten Element weiter
Am Ende wird alles gematcht, und übrig bleibt nur die Partition, in der alle Elemente einzeln und in der ursprünglichen Reihenfolge stehen. Je nach Parität der Größe der ursprünglichen Menge ergibt die Vorzeichensumme die ursprüngliche Aussage
Man weiß nicht einmal, wie viele Terme die Summe über „τ ≤ τ“ hat, und es passt auch nicht dazu, wie damit eine der beiden Seiten aus Punkt 3 aufgestellt und dann die andere Seite gefolgert werden soll
Tatsächlich hat ChatGPT die Möbius-Funktion des Partitionsverbands aus dem Gedächtnis hervorgeholt und ohne Beweis wiedergegeben, und danach nur noch oberflächlich plausibel klingenden Unsinn produziert
Genau diese Möbius-Funktion herzuleiten ist im Grunde der Kern, und die Frage ist fast gleichbedeutend damit, zu beweisen, dass diese Funktion diese Form hat
Außerdem ist auch die allgemeine Formel, die ChatGPT angegeben hat, leicht falsch; sie stimmt nur im für den aktuellen Beweis wichtigen Fall |σ| = 1
Diese Tatsache lässt sich auch ohne den ganzen Apparat der Möbius-Funktion explizit zu verwenden sofort zeigen, indem man N(t,e) als Anzahl der Partitionen von e in t Äquivalenzklassen definiert und mit der Rekursion N(t,e+1)=N(t-1,e)+tN(t,e) eine elementare Induktion durchführt
In diesem Interview stechen drei Dinge hervor
Erstens spricht Tao von project manager mathematicians und entwirft eine Zukunft, in der mathematische Einsichten wie andere gesellschaftliche Ergebnisse „produziert“ werden. Den Grund, warum Mathematik noch nicht derart industrialisiert ist, sieht er im Mangel an Werkzeugen, und AI sowie Proof Assistants könnten hier revolutionär sein. Menschliche Interaktion und Anleitung bleiben jedoch weiterhin nötig
Zweitens gibt es sehr viel implizites Wissen, das nicht in Aufsätzen steht. Dinge wie Intuition oder Wissen über gescheiterte Ansätze sind wichtig, sodass selbst Spitzenmathematiker miteinander sprechen müssen, um nicht dieselben Fehler zu wiederholen
Drittens könnte man leicht glauben, Mathematik sei bereits ausreichend formalisiert, doch in Aufsätzen wird viel gemeinsames Vorwissen vorausgesetzt. Wenn Beweise so formalisiert werden, dass ein Proof Assistant sie verstehen kann, hilft das mehr Menschen, tatsächlich zu verstehen, was vor sich geht
Wie Tao in seinem Vortrag zum Polymath-Projekt gezeigt hat, wird deutlich, dass er immer jemand ist, der nach neuen Wegen für mathematische Forschung sucht
Im Moment könnten solche Projekte nur möglich sein, wenn Fields-Medaillenträger wie Tao oder Scholze die Muße haben, zehnmal so viel Zeit in einen Beweis zu stecken
Ich habe kürzlich mit einem Postdoc einer mathematischen Top-Fakultät gesprochen, und er sagte, in seinem Umfeld nutze niemand lean4 in der tatsächlichen Arbeit
Für Forschende am Anfang ihrer Karriere ist es wahrscheinlich besser, ihrer Intuition zu vertrauen und den Aufsatz einzureichen
Um dieses Thema richtig einzuschätzen, reichen Eindrücke von ein paar Personen nicht aus
Dagegen würde ich erwarten, dass in Bereichen mit stärker intuitivem Stil wie niedrigdimensionaler Topologie weniger Menschen Proof Checkers nutzen
Mit intuitiv ist hier nicht weniger streng gemeint. Ein Bildbeweis für eine Homotopieäquivalenz ist deutlich schwerer in eine Form zu übertragen, die Lean verstehen kann, als eine Auflistung von Ungleichungen
Zur Einordnung: Ich bin in Geometrie/Topologie unterwegs und habe bislang noch niemanden gesehen oder von jemandem gehört, der solche Tools nutzt
https://lean-lang.org/
https://github.com/leanprover/lean4
Der Abschnitt „Wenn eine KI einen unverständlichen und hässlichen Beweis liefert, kann man ihn analysieren. Wenn dieser Beweis 10 Annahmen verwendet, um zu einer Schlussfolgerung zu gelangen: Funktioniert der Beweis immer noch, wenn man eine Annahme entfernt? Diese Wissenschaft existiert noch nicht, weil es noch nicht viele KI-generierte Beweise gibt, aber es wird einen neuen Typ von Mathematikern geben, der KI-generierte Mathematik nimmt und verständlicher macht“ entspricht genau meinen Gedanken zum Design öffentlicher APIs in Code.
Eine Rolle, die traditionell nur erfahrene Entwickler übernommen haben, könnte nun stark vereinfacht und für alle zugänglich werden.