Erdős-Problem Nr. 728 fast autonom von KI gelöst

• Erdős-Problem Nr. 728 wurde kürzlich von KI-Tools fast autonom gelöst und markiert damit einen neuen Meilenstein bei der Automatisierung mathematischer Forschung
• Das Problem war ursprünglich eine 1975 von Erdős, Graham, Ruzsa, Strauss formulierte Frage zur Primfaktorzerlegung von Binomialkoeffizienten und blieb wegen unklarer Bedingungen lange schwer eindeutig zu behandeln
• ChatGPT erzeugte unter angepassten Nebenbedingungen einen Beweis, und Aristotle formalisierte ihn als Lean-Formalbeweis und korrigierte Fehler automatisch
• Anschließend überarbeiteten mehrere Beteiligte den Text mithilfe von ChatGPT in natürlicher Sprache und verbesserten iterativ Versionen mit stärkeren Literaturbezügen und besserer Erzählstruktur
• Terence Tao bewertet den Vorgang als Hinweis darauf, dass die schnelle Erstellung und Korrektur von Beweisen durch KI das Schreiben von Forschungsarbeiten selbst verändern könnte

---

Erdős-Problem Nr. 728 von KI gelöst

• Der jüngste Einsatz von KI-Tools hat bei der Lösung eines Erdős-Problems neue Fortschritte gezeigt, wobei Problem Nr. 728 fast autonom von KI gelöst wurde
  • Nach ersten Versuchen gelang der Erfolg in einer überarbeiteten Version, die Feedback berücksichtigte
  • Das Ergebnis ließ sich in der bestehenden Literatur nicht in identischer Form reproduzieren; es existierten nur ähnliche Resultate mit verwandten Methoden
• Dieser Fall zeigt, dass sich die mathematischen Problemlösungsfähigkeiten von KI in den letzten Monaten tatsächlich verbessert haben
  • Zwar gab es auch früher Fälle, in denen KI Erdős-Probleme löste, doch stellte sich meist heraus, dass die Lösungen bereits in der Literatur vorhanden waren
• Bei diesem Problem war die ursprüngliche Formulierung von Erdős in fehlerhafter Form angegeben worden und wurde erst vor Kurzem in die beabsichtigte Form rekonstruiert
  • Das erklärt, warum es in der vorhandenen Literatur nur wenig einschlägige Forschung gab

Geschichte des Problems und frühe Ansätze

• 1975 untersuchten Erdős, Graham, Ruzsa, Strauss die Primfaktorzerlegung des Binomialkoeffizienten (2n choose n) und formulierten mehrere verwandte Probleme
  • Eines davon fragte nach der Existenz unendlich vieler a, b, n, die die Bedingung a!b! | n!(a+b−n)! sowie a+b > n + C log n erfüllen
  • Allerdings waren mehrere Teile, etwa die Größe von C (klein oder groß), unklar beschrieben
• Vor einigen Monaten fand das AlphaProof-Team eine einfache Lösung des Problems, doch diese entsprach nicht dem beabsichtigten Geist der Frage, weshalb die Zusatzbedingung a,b ≤ (1−ε)n eingeführt wurde
  • Auch eine KI-gestützte Literatursuche fand anschließend kaum einschlägige Arbeiten

Zusammenarbeit von ChatGPT und Aristotle

• Am 4. Januar erzeugte ChatGPT unter den angepassten Nebenbedingungen einen Beweis für den Fall eines kleinen C
  • Dieser Beweis wurde von Aristotle als Lean-Formalbeweis formalisiert
  • Bei einer erneuten Prüfung des Originaltexts stellte sich später heraus, dass die ursprüngliche Arbeit den Fall des kleinen C bereits behandelt hatte
• Ein anderer Teilnehmer wandelte den Lean-Beweis mit ChatGPT in natürliche Sprache um und erstellte durch zusätzliche Dialoge eine verbesserte Version
  • Diese Version schloss einige Lücken im Beweis, litt aber weiterhin unter einem für KI typischen holprigen Stil und fehlenden Literaturverweisen
  • Dennoch erreichte sie ein Maß an Lesbarkeit, bei dem die zentrale Idee nachvollziehbar war

Umfangreiche Überarbeitung und verbessertes Ergebnis

• Durch zusätzliche Prompts erzeugte ChatGPT einen Beweis, der auch auf den Fall eines großen C ausgedehnt war
  • Es gab einige Fehler, doch Aristotle korrigierte sie automatisch und vollendete einen mit Lean verifizierten Beweis
• Ein dritter Teilnehmer komprimierte den Lean-Beweis, worauf ein anderer Teilnehmer in langen Gesprächen mit ChatGPT
  • ihn zu einer ausgereiften Arbeit mit stärkeren Literaturbezügen und besserer narrativer Struktur umschrieb
  • Das Ergebnis wurde als Text bewertet, der weniger nach einem KI-Produkt wirkt und sich in seiner Qualität einer Forschungsarbeit annähert
  • Tao erwähnte, dass er diesen Text im Erdős-Problemforum geprüft habe

Wie KI das Schreiben von Forschungsarbeiten verändert

• Tao ist der Ansicht, dass in der endgültigen Arbeit die Kernelemente weiterhin von Menschen geschrieben werden müssen,
  • bewertet aber die Kombination aus KI und Lean als einen Faktor, der das Tempo beim Schreiben und Korrigieren von Beweisen drastisch erhöht hat
• Bisher kostete es viel Zeit, eine Arbeit gut lesbar zu machen,
  • und auch Überarbeitungen nach Gutachter-Feedback blieben oft auf lokale Änderungen beschränkt
• Nun aber verbinden sich die Fähigkeiten von KI zur Textgenerierung und -überarbeitung mit den Verifikationsfunktionen formaler Beweiswerkzeuge, sodass
  • rasch neue Versionen einer Arbeit mit unterschiedlichem Präzisionsgrad und unterschiedlicher Darstellungsweise erzeugt werden können
• Neben einer einzigen „offiziellen Arbeit“ könnten zudem zahlreiche von KI erzeugte Begleitversionen existieren,
  • die verschiedene Perspektiven und zusätzlichen Wert bieten können

Reaktionen der Community

• Einige Nutzer beschrieben den zusätzlichen Wert von KI-generierten Dokumenten als die Fähigkeit, ein Thema aus einem anderen Blickwinkel zu betrachten
• Andere Mathematiker forderten, die Originalität von KI-Ergebnissen oder die Ähnlichkeit mit bestehender Literatur genauer zu bewerten
  • So wurde etwa eine quantitative Ähnlichkeitsmessung durch Vergleich der Länge formaler Lean-Beweise vorgeschlagen
• In einem weiteren Kommentar hieß es, KI könne Arbeiten wie beim Code-Refactoring global umschreiben,
  • weshalb Forschende sich stärker auf die Gestaltung der Dokumentstruktur auf höherer Ebene konzentrieren sollten
• Einige reagierten skeptisch auf die Möglichkeit, dass KI die Rolle von Mathematikern ersetzen könnte,
  • während andere darin eine neue Chance für Zusammenarbeit und erweitertes Denken sehen