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

[GN⁺]

Hacker-News-Kommentare

• Ich arbeite bei Harmonic und möchte ein paar Missverständnisse über Aristotle ausräumen
  Aristotle nutzt aktiv moderne AI-Techniken, einschließlich Language Modeling
  Wenn man einen informellen Beweis auf Englisch eingibt, ist die Wahrscheinlichkeit hoch, dass er nach Lean übersetzt werden kann, sofern der Beweis korrekt ist. Das ist also ein starkes Signal dafür, dass der englische Beweis solide ist
  Sobald er in Lean formalisiert ist, gibt es keinen Zweifel mehr an der Korrektheit des Beweises. Das ist unser Kernansatz — wenn wir die Antwort durch AI-gestützte Suche finden, können wir die Korrektheit des Ergebnisses unabhängig von seiner Komplexität garantieren

  • Ich frage mich, wie geprüft wird, ob ein von AI nach Lean übersetzter Beweis wirklich die korrekte Formalisierung des Problems ist. Da generative AI in anderen Bereichen sehr gut darin ist, plausible Unwahrheiten zu erzeugen, würde mich interessieren, ob das hier auch passieren kann
  • Ich frage mich, ob es Versuche gibt, diese Technik auf Softwareverifikation anzuwenden
    Rust verwendet einen festen Regelsatz, um Speichersicherheit zu garantieren, aber diese Regeln sind einfach und restriktiv. Es wäre wirklich großartig, wenn ein System wie Aristotle in den Compiler integriert würde, sodass Code automatisch akzeptiert wird, wenn sich seine Korrektheit beweisen lässt
  • Bei jedem neuen LLM bin ich unsicher, ob es sich um echten Fortschritt oder bloßes Benchmark-Hacking handelt, aber die Formalisierung mathematischer Beweise scheint mir ein guter Indikator für echte Fortschritte zu sein
    Ich frage mich, wie lange Harmonic brauchen wird, um den Großteil der von Menschen geschriebenen Mathematik formalisieren zu können. Der Konkurrent Christian Szegedy meinte, das sei noch dieses Jahr möglich
  • Du hast gesagt, dass ein korrekter englischer Beweis mit hoher Wahrscheinlichkeit nach Lean übersetzt werden kann. Ich frage mich, ob das je nach Schwierigkeitsgrad des mathematischen Teilgebiets variiert. Soweit ich weiß, sind viele Forschungsgebiete selbst für Menschen noch schwer zu formalisieren
  • Die Voraussetzung „wenn die Aussage korrekt formalisiert wurde“ klingt nach einer ziemlich großen Annahme. Wie der jüngste Navier-Stokes-Fall gezeigt hat, ist schon die Formalisierung selbst nicht einfach

• Nach Terence Taos Erklärung sieht es so aus, als habe ein Mensch Ergebnisse zwischen zwei AI-Tools hin- und hergereicht, wobei die AI Lücken füllte, die der Mensch gefunden hatte
  Das wirkt eher wie eine Zusammenarbeit zwischen Mensch und AI als wie eine vollständig autonome Lösung. Also ein Modell, bei dem der Experte führt und die AI unterstützt

  • Ja, ich verstehe es auch so, dass Aristotle, ChatGPT und ein sehr fähiger Nutzer dabei interagiert haben
  • Ich habe gehört, dass Tao oder die Community die Lücken nicht direkt selbst gefunden haben, sondern einen automatischen Beweisprüfer verwendet haben. Eher so etwas wie 90 % AI / 10 % Mensch
  • Auf Reddit gibt es eine ausführliche Erklärung des Autors — Reddit-Beitrag
  • Wer das Niveau menschlicher Expertise und den Aufwand verstehen will, sollte den Thread im Erdős-Probleme-Forum lesen
  • Zur Einordnung: Die Website wurde vom Mathematiker Thomas Bloom erstellt, und ChatGPT half bei der technischen Einrichtung (Zitat aus den FAQ)

• Das Rekonstruieren bestehender Beweise oder ihre Neukombination auf neue Weise ist für Menschen oft ein langweiliger oder komplexer Prozess, aber AI kann das mit übermenschlicher Geschwindigkeit erledigen
  Dieser Ansatz dürfte schon vor AGI enormes Potenzial eröffnen. Es scheint eine Zeit zu kommen, in der Mathematiker AI als Werkzeug nutzen, um schwierige Probleme wie die Millennium-Probleme anzugehen

  • Ich denke nicht, dass es eine klare Grenze zwischen der Rekonstruktion bestehender Beweise und der Schaffung völlig neuer Mathematik gibt
  • Da Mathematik logisch ist, dürfte es bereits viele Algorithmen für eine solche Suche geben, daher wirkt das nicht wie ein bloßes Suchproblem
  • Dem Teil über die Rekonstruktion bestehender Beweise stimme ich zu. Die Ergebnisse von LLMs zu validieren ist immer noch langweilige Arbeit, aber immer noch besser, als alles von Hand zu machen
    Der eigentliche Wert von LLMs liegt darin, bei sprachlich ausdrückbaren Themen neue Perspektiven vorzuschlagen
  • Ich nenne dieses Phänomen „wissenschaftliches Refactoring“. Zum Beispiel kann AI automatisch Experimente durchführen, bei denen man eine Konstante ändert und die Logik neu entfaltet
  • Wenn eine AI komplexe Theoreme beweisen kann und das noch nicht AGI ist, was wäre dann überhaupt AGI?

• Im Erklärtext der Person, die das Problem tatsächlich gelöst hat, ist besonders beeindruckend, dass das Ergebnis ohne riesige Pipeline, nur mit wenigen Prompts erzielt wurde
  Neuere Modelle verwenden deutlich mehr Rechenressourcen, daher wirkt das eher wie ein Ergebnis auf Untergrenzenniveau

• Terence Tao hat eine Wiki-Seite mit dem Titel „AI contributions to Erdős problems“ erstellt
  Laut der GitHub-Seite und diesem Mathstodon-Beitrag ist dieses Ergebnis (Problem 728) der erste „grüne Eintrag“ auf dieser Seite, also der erste Fall, den AI tatsächlich gelöst hat

  • Interessanterweise wurden die meisten formalisierten Beweise mit AI in Abschnitt 6 des Wikis erst in den letzten Monaten fertiggestellt. Die Zukunft ist vielversprechend

• Ich frage mich, ob auch Experten in komplexen Bereichen wie Physik oder Mathematik mit AI sprechen und sich helfen lassen

  • Ich habe in reiner Mathematik promoviert und arbeite jetzt als Data Scientist. Für Literaturrecherche oder um sich schnell in weniger vertraute Mathematik einzuarbeiten, ist AI sehr hilfreich
    Je nach Fachgebiet nimmt der Nutzen etwa in dieser Reihenfolge ab: Programmierung > angewandtes ML > Statistik/angewandte Mathematik > reine Mathematik
  • Ich habe zwar keinen Physik-Hintergrund, aber dank AI brauche ich viel weniger Zeit, um die nötigen Formeln oder Paper zu finden. Die Ergebnisse muss man allerdings immer überprüfen
  • Aus der Perspektive von Forschung an Deep-Learning-Modellen und neuen Attention-Architekturen ist ChatGPT sehr nützlich für die Papersuche und das Erkunden verwandter Ideen
  • Als Mathematik-Hobbyist geben mir LLMs Feedback zu meinen Versuchen oder lotsen mich zu bestehenden Lösungen. Für Mathematik als Spiel ist das ein ziemlich unterhaltsames Werkzeug
  • Ich forsche in algebraischer Geometrie, und außer bei der Literaturrecherche hilft es bislang noch nicht besonders viel. Zwischen den Modellen gibt es große Unterschiede

• Man kann Aristotle jetzt direkt ausprobieren — https://aristotle.harmonic.fun/

  • Ich frage mich auch, ob die AI mit dem formal-conjectures-Datensatz von DeepMind getestet wird
  • In der Dokumentation steht „uvx aristotlelib@latest aristotle“, aber korrekt ist eigentlich „uvx --from aristotlelib@latest aristotle“
    Außerdem ist der Link zur persönlichen Stanford-Seite falsch (das www muss entfernt werden)
  • Das ist interessant genug für einen eigenen HN-Thread. Wenn ich CEO wäre, würde ich direkt selbst einen Vorstellungsbeitrag schreiben (Referenzlink)

• Dieses Ergebnis betrifft einen Satz über ganze Zahlen, also einen Bereich, den die Mathlib-Infrastruktur gut unterstützt
  Die verwendeten Definitionen sind auch nicht komplex, daher ist die Erfolgswahrscheinlichkeit bei dieser Art von Beweis hoch. Trotzdem ist es eine wirklich erstaunliche Leistung

• Das ist ein Beispiel für das Potenzial spezialisierter AI-Ansätze jenseits von LLMs
  Das Aristotle-Paper ist auf arXiv:2510.01346 verfügbar
  Nur weil etwas eine Transformer-Architektur nutzt, ist es noch kein LLM — wenn es nicht mit Sprachdaten trainiert wurde, sollte man es nicht LLM nennen

  • Die Verwirrung scheint daher zu kommen, dass viele „LLM“ und „GenAI“ synonym verwenden
  • Du hast von einem „Nicht-LLM-Ansatz“ gesprochen, aber wurde in der Praxis nicht ChatGPT verwendet?
  • Doch, tatsächlich wurde ChatGPT verwendet
  • Laut dem Paper sind an allen drei Stufen große transformerbasierte LLMs beteiligt
    1. Sie übernehmen die Policy-/Value-Funktionen in der Monte Carlo Graph Search
    2. Das informelle Schlussfolgerungssystem nutzt chain of thought
    3. AlphaGeometry verwendet ebenfalls ein neuro-symbolisches Sprachmodell
       Mit anderen Worten: Alle Stufen sind LLM-basiert

• 2026 wird AI sich wohl zunehmend mit ungelösten Problemen der Mathematik beschäftigen
  Auch dieser Fall war nicht vollständig autonom, aber nach menschlichem Feedback hat die AI das Problem fast eigenständig gelöst
  Ich denke, die Debatte darüber, dass „LLMs nur stochastische Papageien“ seien, ist jetzt vorbei. Künftig wird sich die eigentliche Diskussion darum drehen, wie man sie praktisch einsetzt

  • 2026 dürfte es in der Mathematik explosive Fortschritte geben
  • Dieses Ergebnis ist wahrscheinlich ein Remix ähnlicher Beweise aus den Trainingsdaten, aber gerade diese Remix-Fähigkeit ist mächtig
  • Es braucht weiterhin unabhängige Verifikation. Allein den Aussagen eines Unternehmens kann man nur schwer vertrauen