In sechs Stunden wurde ein 30 Jahre altes mathematisches Problem gelöst, und Aristoteles wurde über Nacht berühmt.

Wurde ein 30 Jahre altes ungelöstes mathematisches Problem tatsächlich von einer KI bewiesen?!

Gerade jetzt ist auf 𝕏 (ehemals Twitter) eine Debatte los -

Das mathematische KI - Modell von Harmonic hat unabhängig das Erdős - Problem #124 bewiesen, ein Problem, das von Mathematikern seit fast 30 Jahren ratlos beiseite gelegt wurde.

Sebastien Bubeck, der ehemalige Vizepräsident für KI bei Microsoft und derzeit Forscher für AGI bei OpenAI, hat diese Nachricht begeistert geteilt und erklärt:

Die Lösung wurde zu 100 % von der KI generiert und benötigte insgesamt 6 Stunden.

Selbst ein Spitzenmathematiker wie Terence Tao hat sich an der Diskussion beteiligt. Nach einem Vergleich der tiefgreifenden Forschungswerkzeuge von Gemini und ChatGPT stellte er fest, dass das Harmonic - Modell bei der Lösung dieses Problems besser abgeschnitten hat.

Was für ein Problem ist das eigentlich? Und wie hat das Harmonic - Modell seine "Zauberkünste" ausgeführt?

Lasst uns weiter gucken -

Die KI hat eine vereinfachte Version des Erdős - Problems #124 bewiesen

Zunächst müssen wir darauf hinweisen, dass wir erst nach den Diskussionen verschiedener Experten erkannt haben -

Das Harmonic - Modell hat nicht das originale Erdős - Problem #124 bewiesen, sondern eine vereinfachte Version.

Das Erdős - Problem #124 erfordert den folgenden Beweis:

Verständlich ausgedrückt:

Nehmen wir an, Sie haben k verschiedene "Basisgeneratoren", die jeweils den Zahlen d1, d2, …, dk entsprechen.

Die Spielregeln lauten wie folgt: 1) Sie können aus jeder von den Generatoren erzeugten Zahlenliste maximal eine Zahl auswählen; 2) Dann addieren Sie alle von Ihnen ausgewählten Zahlen; 3) Schließlich prüfen Sie, ob Sie so genau Ihre Zielzahl erhalten können.

Das Kernproblem ist -

Wenn Ihre "Basisgeneratoren" eine bestimmte Bedingung erfüllen, nämlich 1/(d1 - 1)+1/(d2 - 1)+…+1/(dk - 1) ≥ 1, können dann alle hinreichend großen ganzen Zahlen mit diesen Regeln zusammengesetzt werden?

Bis jetzt kann der Fortschritt bei diesem Problem wie folgt zusammengefasst werden:

Das heißt, dieses Problem hat sich im Laufe von Jahrzehnten in eine schwere und eine einfache Version entwickelt.

Im originalen [BEGL96] darf der Herausforderer die Zahl 1 nicht verwenden und muss zusätzlich die gcd - Bedingung erfüllen (es gibt keine "doppelten Perioden" zwischen den Basen). Schließlich wurde nur festgestellt, dass die Vermutung für die bestimmte Menge {3, 4, 7} gilt.

Wenn die Bedingungen gelockert werden (die Zahl 1 darf verwendet werden und die zusätzliche gcd - Bedingung muss nicht erfüllt werden), hat das Harmonic - Modell erfolgreich bewiesen, dass alle großen ganzen Zahlen zusammengesetzt werden können, wenn die oben genannte bestimmte Bedingung erfüllt ist, und der Beweis wurde durch die formale Überprüfung in Lean bestätigt.

Das Beweisschema des Harmonic - Modells ist wie folgt. Experten haben angegeben, dass dieses Schema überraschend einfach ist.

Allerdings hat Boris Alexeev, der dieses vereinfachte Problem #124 mit dem Harmonic - Modell bewiesen hat, auch ergänzt:

Im Projekt "formalisierte Vermutung" gab es ursprünglich eine formale mathematische Formulierung dieser Vermutung. Doch es gab einen Tippfehler: In der Anmerkung stand ≥1, während im entsprechenden Lean - Programmcode =1 stand. Dieser Fehler hat die Bedingungen der ursprünglichen Formulierung geschwächt, da nur der Fall des Gleichheitszeichen abgedeckt wurde, während der Fall des größer - als - Zeichens ausgelassen wurde.

Daher habe ich diesen Fehler korrigiert und die Teile, die ich für unnötig hielt, aus der ursprünglichen Formulierung entfernt. Schließlich hat die KI diese kürzere und genauere Version erfolgreich bewiesen.

Zusammengefasst hat Harmonic die vereinfachte Version des Problems #124 bewiesen, während die schwere Version immer noch ungelöst ist.

"Die Ära der Vibe - Beweise ist angebrochen"

Trotzdem haben Experten das Potenzial von KI - Modellen bei der Lösung mathematischer Probleme bestätigt.

Unter Bezugnahme auf das Konzept des Vibe Coding im Programmierbereich (zuerst von dem KI - Guru Karpathy vorgeschlagen) hat der Mitbegründer und CEO von Harmonic begeistert erklärt:

Wir stehen am Rande einer tiefgreifenden Veränderung im mathematischen Bereich. Die Ära der Vibe - Beweise ist angebrochen.

Basierend auf seiner Aussage haben wir uns auch das Unternehmen hinter dem Harmonic - Modell angesehen, da es in Terence Taos Augen diese Zeit ChatGPT und Gemini besiegt hat.

Nach öffentlichen Informationen ist das Unternehmen hinter dem Modell Harmonic, und sein Ziel ist sehr klar:

Die weltweit fortschrittlichste mathematische Inferenzmaschine zu entwickeln.

Die beiden Mitbegründer sind Tudor Achim und Vlad Tenev.

Der CEO Tudor Achim hat einen Bachelor - Abschluss in Informatik von der Carnegie Mellon University und studiert derzeit auch für einen PhD in Informatik an der Stanford University, befindet sich aber derzeit im "on leave" - Status.

Im Jahr 2023 gründete er gemeinsam mit Vlad Tenev Harmonic und wollte damals die weltweit fortschrittlichste Inferenzmaschine entwickeln.

Zuvor war er auch Mitbegründer und CTO einer Firma für die Entwicklung von Fahrerassistenzsystemen (Helm.ai).

Der Exekutivvorsitzende Vlad Tenev hat einen Bachelor - Abschluss in Mathematik von der Stanford University und einen Master - Abschluss in Mathematik von der University of California, Los Angeles.

Außer als Mitbegründer und Exekutivvorsitzende bei Harmonic ist er derzeit auch CEO der Finanzfirma Robinhood Markets.

Nach öffentlichen Informationen auf der offiziellen Website hat Harmonic vor etwa einer Woche eine Serie - C - Finanzierung in Höhe von 120 Millionen US - Dollar (etwa 850 Millionen Yuan) abgeschlossen.

Diese Runde wurde von Ribbit Capital geleitet, und der Unternehmenswert erreichte 1,45 Milliarden US - Dollar (etwa 10,3 Milliarden Yuan).

Das Flaggschiffmodell von Harmonic ist das hier verwendete Aristotle - Modell (manchmal auch "Aristoteles" genannt). Es ist das erste Modell, das bei der Internationalen Mathematikolympiade 2025 formalisierte Lösungen für fünf der Aufgaben vorgelegt hat.

Aristotle hat eine Leistung auf Gold - Niveau erreicht, während es die Genauigkeit gewährleistet und Halluzinationen vermeidet.

Laut Vlad Tenev wurde das für diese Lösung verwendete Aristotle - Modell aktualisiert und hat eine stärkere Inferenzfähigkeit und eine natürliche Sprachschnittstelle.

Es ist vorhersehbar, dass mit dem fortschreitenden Erfolg von KI bei der Lösung komplexer mathematischer Probleme immer mehr seit Jahrhunderten ungelöste Probleme neu beleuchtet und möglicherweise gelöst werden.

Wie auch immer, in der Welle der KI gibt es keinen Rückzieher.

Referenzlinks:

[1]https://x.com/i/trending/1994986636623724980

[2]https://www.erdosproblems.com/forum/thread/124#post-1892

[3]https://x.com/thomasfbloom/status/1995094668879462466

Dieser Artikel stammt aus dem offiziellen WeChat - Account "QbitAI", Autor: Yishui. 36Kr hat die Veröffentlichung mit Genehmigung erhalten.