Auf der Erdős-Problem-Website wird KI-Unterstützung allmählich zum Alltag

• Beim Lösungsprozess von Erdős-Problem #367 spielte ein KI-Tool eine Schlüsselrolle; berichtet wird von einem Fall der Zusammenarbeit zwischen menschlichen Mathematikern und KI
• Wouter van Doorn legte ein von Menschen erzeugtes Gegenbeispiel für den zweiten Teil des Problems vor, anschließend erzeugte Gemini Deepthink einen vollständigen Beweis der betreffenden Kongruenz
• Terence Tao übertrug Geminis auf p-adischer algebraischer Zahlentheorie basierenden Beweis in eine einfachere Form und veröffentlichte ihn; später erwähnte er die Möglichkeit einer Lean-Formalisierung
• Boris Alexeev schloss mit Harmonics Tool Aristotle die Lean-Formalisierung ab und überprüfte die endgültige Aussage zur Vermeidung von KI-Missbrauch manuell
• Diese Abfolge von Schritten zeigt, dass KI-Unterstützung in der mathematischen Forschung zunehmend zu einem Standardverfahren wird

---

Fallbeispiel für KI-Zusammenarbeit bei Erdős-Problem #367

• Am 20. November präsentierte Wouter van Doorn ein Gegenbeispiel für den zweiten Teil des Problems, das auf der Annahme beruhte, dass eine bestimmte Kongruenz gilt
  • Er bat andere Teilnehmende, die Gültigkeit dieser Kongruenz zu überprüfen
• Einige Stunden später legte Terence Tao das Problem Gemini Deepthink vor und erhielt nach etwa 10 Minuten einen vollständigen Beweis der Kongruenz sowie eine Bestätigung der gesamten Argumentation
  • Geminis Beweis nutzte p-adische algebraische Zahlentheorie, und Tao wandelte ihn in einen einfacheren elementaren Beweis um und veröffentlichte ihn auf der Website
  • Tao erwähnte, dass sich dieser Beweis in Lean per „vibe formalizing“ formalisieren lassen könnte

Lean-Formalisierung und Verifikation

• Zwei Tage später schloss Boris Alexeev mit Harmonics Tool Aristotle die Lean-Formalisierung ab
  • Um KI-Missbrauch zu verhindern, wurde die endgültige Aussage manuell direkt formalisiert
  • Der gesamte Prozess dauerte etwa 2 bis 3 Stunden, und das Ergebnis wurde online veröffentlicht
• Tao führte anschließend mit KI eine Literaturrecherche durch; es gab zwar einige verwandte Arbeiten, aber nichts, das direkt mit Problem #367 zusammenhing

Reaktionen und Diskussionen in der Community

• Einige Nutzer verfolgten Taos Update mit Interesse als Beispiel für den aktuellen Einsatz von KI in der akademischen Mathematik
• Andere äußerten sich kritisch zum formalistischem Ansatz von Lean und wiesen darauf hin, dass mathematisches Verständnis Kompression sei, während Lean dies in Details auf niedriger Ebene dekomprimiere
  • Das zugehörige Dokument “Against Lean: Why Proof Assistants Formalize the Wrong Thing” argumentiert, dass Lean und ähnliche Proof Assistants das Wesen der Mathematik falsch erfassen
• Ein weiterer Nutzer erwähnte Genauigkeitsprobleme in KI-Gesprächen und bewertete die Nutzung als fein abstimmungsbedürftig, aber unterhaltsam

[GN⁺]

Hacker-News-Kommentare

• Es ist eine erstaunliche Erfahrung, einem KI-Assistenten ML-Papers mit starkem Mathematikbezug zu geben und dafür einfache Erklärungen oder Pseudocode zurückzubekommen
  Für jemanden wie mich, der das an der Universität Gelernte über 25 Jahre lang nie gebraucht hat, ist das eine enorme Hilfe

  • Ich frage mich, wie man überprüft, ob diese Erklärungen korrekt sind. Mathematische Definitionen haben oft sehr subtile Nuancen
  • Genau hier, finde ich, glänzen LLMs beim Lernen
    Man kann ein Paper in Claude laden, sich erst einen Überblick geben lassen und dann mit Rückfragen weitermachen
    Selbst in Bereichen wie Biologie, die ich weder im Bachelor noch im Master gelernt habe, konnte ich tief einsteigen, fast wie in einem Gespräch mit einem kundigen Tutor
  • Mathematische Notation ist stark kontextabhängig, deshalb kann man die Struktur oft viel schneller erfassen, wenn man ein LLM bittet, sie in eine kontextarme Sprache wie Lisp zu übersetzen

• Ich hoffe, dass Forschende und Unternehmen in der wissenschaftlichen Arbeit mehr Produktivitätsgewinne erzielen
  Selbst ein unvollkommener Assistent kann genug Hebelwirkung liefern

  • Es gibt eine von Tao erwähnte Beta einer Formalisierungs-App für iOS → Aristotle
    Angeblich ein Startup, das vom Robinhood-CEO gegründet wurde

• „Vibe formalizing“ wirkt wie die logische Erweiterung von „vibe engineering“ und „vibe coding“
  Wenn die Teile eines Problems nicht sauber zusammenpassen, ist ein Ansatz interessant, der informelle Methoden und mathematische Strenge verbindet, fast wie „Move 37 as a Service“

  • Ich war früher einmal bei einem polyhedral-compilation-Paper an einer Stelle hängengeblieben, und ChatGPT hat den Reasoning-Prozess gut angeleitet
    Natürlich lagen auch Fehler darin, aber indem es meine Verwirrung gespiegelt und mit mir gesprochen hat, konnte ich mein Verständnis vertiefen
    KI ist besonders stark darin, die Punkte der Verwirrung bei Nutzern zu erkennen

• Ich habe die Geschichte über die Aussprache des Namens des ungarischen Mathematikers Erdős gehört
  Im Ungarischen stimmen Schreibweise und Aussprache fast immer überein, aber bei Namen gibt es Ausnahmen
  Auf Englisch klingt es wohl ungefähr wie „airdish“

  • Ő ist einfach ein œ(oe)-Laut. Das -y in ungarischen Namen ist eine Spur der -i-Endung, die früher adlige Herkunft markierte
    Beispiele: Görgey, Széchényi, Lánczos usw.
    Die Reihenfolge ungarischer Namen ist wie im Japanischen Nachname-Vorname (big endian). Zum Beispiel: „Erdős Pál“, „Neumann János“
  • Ich habe einmal ein scherzhaftes Gedicht von 1960 an einem schwarzen Brett des Mathematik-Fachbereichs gesehen — darin ging es um den Witz, dass ein von Erdos verfasstes Paper den Satz „Kreise sind rund“ widerlegt habe
  • Da Aussprachezeichen (diakritische Zeichen für die Aussprache) je nach Sprache Unterschiedliches bedeuten, finde ich es seltsam, ungarische Zeichen unverändert in englische Sätze zu setzen
  • Anfangs kam mir die Aussprache „airdish“ merkwürdig vor, aber als ich versucht habe, die Endung „os“ zu palatalisieren, klang es plausibel
  • Vielleicht weil ich kein Amerikaner bin, aber bei solchen Aussprachefragen scheint sich niemand wirklich darum zu kümmern

• Ich finde es interessant, dass es in den Kommentaren Reaktionen mit einer anti-Lean-Tendenz gibt

  • Ich bin kein Mathematiker, aber ich würde gern wissen, ob dieses anti-Lean-Material vertrauenswürdig ist
    Wird da einfach nur ein anderer Ansatz beworben, oder steckt eine philosophische Ablehnung von Lean dahinter?
  • Berühmte Leute wie Tao ziehen naturgemäß viel Aufmerksamkeit von Exzentrikern und Verschwörungstheoretikern auf sich

• Meine Erfahrungen mit KI in der Forschungsmathematik sind gemischt
  Manchmal vervollständigt sie nichttriviale Argumentationen automatisch, in anderen Bereichen verirrt sie sich völlig
  Ich denke, wir sind noch an einem Punkt, an dem KI eher nur als Hilfswerkzeug nützlich ist, statt Mathematiker zu ersetzen

  • Ich hatte eine ähnliche Erfahrung. Ich habe ihr in einem Paper ein einfaches Problem zur Permutationsberechnung gegeben, und am Ende hat es länger gedauert, als es selbst zu lösen
    Auch beim Coding hat sie manchmal banale Bugs nicht gefunden, war aber bei komplexeren Aufgaben eine große Hilfe
    Letztlich sind diese Werkzeuge noch weit davon entfernt, Experten zu ersetzen, und Übertreibung im Marketing kann das Vertrauen eher beschädigen
    Wie man sagt: Wenn man den Mond verspricht, sollte man auch den Mond liefern — realistische Erwartungen sind wichtig

• Ich kann kaum glauben, dass ich noch erlebe, wie man wie in Star Trek sagen kann: „Computer, visualisiere den Beweis dieses mathematischen Problems für mich“
  Schön wäre es auch, wenn „Beam me up Scotty“ möglich wäre

  • Aber wenn man dabei jedes Mal sterben könnte, wäre das wohl eher unerquicklich

• Heute Abend habe ich beim Fahren mit ChatGPT über die Details von LLVM- und GCC-Pipeline-Schedulern gesprochen
  Das hat meine Produktivität deutlich erhöht, und meine experimentellen Notizen zu Compilern wurden automatisch geordnet
  Früher wäre das völlig unvorstellbar gewesen

  • Meiner Erfahrung nach ist es gut möglich, dass LLMs bei einigen Details falschliegen
    Natürlich können die Ergebnisse je nach Person unterschiedlich ausfallen

• Wenn man eine KI Erdos nennt, hätten wir wohl alle eine Erdos-Zahl von 1

  • Oder es wirkt wie ein Nachfolger von DR-DOS
  • Tatsächlich gibt es bereits ein Produkt namens Erdos, eine KI-integrierte IDE

• Beeindruckend ist, wie er vorhandene Frontier-Tools gut eingesetzt hat, um ein kollaboratives Umfeld für mathematische Forschung zu schaffen

  • Zum Glück ist Mathematik ein Bereich, in dem Idolisierung oder Beliebtheitswettbewerbe nicht über die Wahrheit eines Ergebnisses entscheiden
    Deshalb halte ich Mathematik noch immer für eine der seltenen Disziplinen, die weitgehend frei von pseudowissenschaftlichem Einfluss sind