- Ein ungelöster Teil des von Donald Knuth formulierten Hamilton-Zerlegungsproblems wurde durch die Zusammenarbeit von Menschen und KI weitergehend gelöst
- Claude fand eine Lösung für ungerade m, die „Claude’s Cycles“ genannt wurde; später wurden 996 von 11.502 Zyklen auf alle ungeraden m verallgemeinert
- Dr. Ho Boon Suan erstellte mit GPT-5.4 Pro einen 14-seitigen Beweis für gerade m≥8 und führte eine rechnerische Verifikation bis m=2000 durch
- Dr. Keston Aquino-Michaels entdeckte mit einem Multi-Agenten-Workflow aus GPT und Claude eine einfache Konstruktionsmethode für sowohl ungerade als auch gerade m
- Dr. Kim Morrison formalisiert Knuths Lösung mit dem Beweisassistenten Lean und vervollständigt damit ein kollaboratives Ökosystem aus Mensch, KI und Beweiswerkzeugen
Erweiterte Zusammenarbeit bei der Lösung des Problems „Claude’s Cycles“
- Ein ungelöster Teil des von Donald Knuth formulierten Hamilton-Zerlegungsproblems wurde durch die Zusammenarbeit von Menschen und KI gelöst
- Zunächst fand Claude nach etwa einer Stunde Suche eine Lösung für ungerade m, die von Knuth „Claude’s Cycles“ genannt wurde
- In der später aktualisierten Arbeit zeigte sich, dass es im Basisfall m=3 genau 11.502 Hamilton-Zyklen gibt, von denen sich 996 auf alle ungeraden m verallgemeinern lassen
- Knuth bestätigte darunter 760 gültige Zerlegungen vom „Claude“-Typ
- Für gerade m konnte Claude die Lösung nicht abschließen, doch Dr. Ho Boon Suan verfasste mit GPT-5.4 Pro einen 14-seitigen Beweis für m≥8 und führte eine rechnerische Verifikation bis m=2000 durch
- Anschließend entdeckte Dr. Keston Aquino-Michaels mithilfe eines Multi-Agenten-Workflows mit GPT und Claude eine einfache Konstruktionsmethode, die sowohl auf ungerade als auch auf gerade m anwendbar ist
- Dr. Kim Morrison formalisierte und verifizierte Knuths Lösung für den ungeraden Fall im Beweisassistenten Lean
- Dadurch entstand letztlich ein vollständiges mathematisches Kooperationsökosystem, in dem Menschen, mehrere KI-Systeme und formale Beweiswerkzeuge parallel zusammenarbeiten
- Diese Abfolge zeigt, wie sich die Lösung eines einzelnen Problems durch eine KI zu einem neuen Modell mathematischer Forschung entwickelte, das auf der Zusammenarbeit von mehreren KIs, Menschen und Beweisassistenten beruht
- Die neueste Arbeit ist auf der Stanford-CS-Faculty-Website veröffentlicht: www-cs-faculty.stanford.edu/~knuth/papers/
1 Kommentare
Hacker-News-Kommentare
Ich habe immer gesagt, KI wird eher eine Fields-Medaille gewinnen, als einen McDonald’s zu betreiben
Mathematik fühlt sich für Menschen so schwer an, wie Schrauben mit einem Hammer hineinzudrehen
LLMs sind stark in flacher, aber breiter Suche und entdecken viele neue mathematische Muster
Ich erwarte, dass man künftig statt LLMs auf AlphaGo-artiges Reinforcement Learning auf Basis von Lean-Syntaxbäumen umsteigen wird
Wenn man die „10 Tricks“, die Mathematiker verwenden, als latente Vektoren kodieren kann, ist das Spiel vorbei
Wir denken so, dass wir über geometrische Analogien algebraische Geometrie auf Probleme der Zahlentheorie anwenden
Eine mit Lean-Bäumen trainierte KI könnte sogar ein breiteres System von Intuitionen als Menschen haben
Wie das Beispiel von StockFish im Schach zeigt, wäre es lohnend, diesen Ansatz aus Sicht der mechanistischen Interpretierbarkeit (mechanistic interpretability) zu untersuchen
Tricks abzurufen können LLMs schon jetzt gut
Aber den Teil, in dem das Problem richtig dargestellt wird, übernehmen nach wie vor Menschen, und das ist natürlich
Ich würde gern meine eigene Variante hinzufügen: „Der letzte Beruf, der automatisiert wird, ist QA“
Diese Technologiewelle hat uns gezwungen, das Wesen von Wissensarbeit neu zu durchdenken, und dadurch werden wir schärfer werden
Seit ich einmal das 4chan-Sprichwort „trolls trolling trolls“ gelernt habe, betrachte ich Interaktionen im Internet immer mit Misstrauen
Ich hatte schon das Gefühl, Reddit sei bereits ein „totes Internet“, aber wenn ich diesen Thread sehe, kann ich jetzt nicht mehr unterscheiden, wer Bot und wer Mensch ist
Deshalb habe ich einen Dienst namens RememberBuddy gebaut — ein Ort, an dem man Einsichten aus dem Alltag speichern kann, damit man sie nicht vergisst
Die Entwicklung von KI-Mathematik scheint der Bahn zu folgen, die Greg Egan in den 90ern in seinen Romanen vorausgesehen hat
Das Wesen der Mathematik wird sich nicht ändern, aber das „Warum“ wird sich ändern
In Egans Diaspora werden mathematische Entdeckungen beschrieben, als würde man in einem Salzbergwerk Edelsteine abbauen
Manche suchen die reine Schönheit dieser Edelsteine, andere ihren praktischen Wert
Orte wie das Institut, das Terence Tao derzeit aufgebaut hat, berühren bereits diese Zukunft
Kurzfristig wird solche Forschung die Fähigkeit von KI-Systemen, präzise Informationen zu erzeugen, stark verbessern
Manche Leute denken, Wissensentdeckung sei bloß das Nachahmen vergangenen Verhaltens, aber ich sehe das nicht so
Wenn ein Experte das Modell gut lenkt, lassen sich die meisten Probleme lösen
Als Werkzeug, das dem Experten lästige Arbeit abnimmt, ist das Modell hervorragend, aber bei komplexen Problemen gibt es weiterhin blinde Flecken
Ich habe im Paper einen Teil des System-Prompts gesehen,
dort gab es die Regel, nach jedem Ausführen von exploreXX.py sofort plan.md zu aktualisieren
Ich frage mich, warum solche Prompts die Leistung bei fortgeschrittener Problemlösung verbessern
Wir kommen der Vision des OpenAI-CEO von „Intelligenz als Abonnement (intelligence as a subscription)“ immer näher
Dass man weniger zwischen Tabs wechseln muss, wird unterschätzt
Bei der Hälfte aller KI-Tools geht es nicht um ein UX-Problem, sondern um den Kampf, stabilen Zugriff auf das Modell sicherzustellen
„Wenn man 100 Affen 100 Gewehre und Baumaterial gibt, werden sie dann ein Haus bauen oder eine Bank ausrauben?“
Falls so ein Ergebnis herauskäme, würde ich fragen, ob das beabsichtigtes Verhalten ist
Ich habe diesen Tweet gesehen