Ein 30-jähriges mathematisches Rätsel wurde von KI in nur sechs Stunden gelöst. Terence Tao: Alle ChatGPT-ähnlichen Systeme haben versagt.

Letzte Nacht hat die Mathematikwelt in Aufruhr geraten! Der KI-Mathematiker "Aristoteles" hat in nur sechs Stunden die vereinfachte Version eines 30-jährigen Problems mit einem Klick gelöst, was von Terence Tao hoch gelobt wurde. Die Ära der Intuitionsbeweise in der Mathematik ist da.

Ein 30 Jahre lang ungelöstes mathematisches Problem ist endlich gelöst!

Der von HarmonicMath entwickelte KI-Mathematiker "Aristoteles" (Aristotle) hat das Erdős-Problem #124 vollständig unabhängig gelöst.

Es hat im Lean-Beweissystem nur sechs Stunden gebraucht, und die Überprüfung hat nur eine Minute gedauert.

Ohne jegliche menschliche Unterstützung. Dieser Moment kann als der "Mondlandungs"-Moment der Mathematik bezeichnet werden.

Vlad Tenev, der Gründer von HarmonicMath, sagte: "Die Mathematikwelt steht vor einem gewaltigen Wandel. Die Ära der Intuitionsbeweise ist da!"

Selbst der Fields-Medaille-Träger Terence Tao hat den KI-Mathematiker "Aristoteles" hoch gelobt.

Die Ära, in der KI Mathematik entdeckt, hat offiziell begonnen.

Ein 30-jähriges Problem gelöst - die KI hat es geschafft

Seit langem ist die "Problemliste" des Mathematikers Erdős Pál wie der Mount Everest des Wissens, der die Grenzen des Menschen herausfordert.

Die Preise für die ungelösten Probleme reichen von einigen Dollar bis zu mehreren tausend Dollar.

Ihre symbolische Bedeutung ist weitaus größer als ihr praktischer Wert, und sie sind für unzählige Mathematiker wie geistige Orden.

Seit 30 Jahren, seit das Problem #124 (Erdős #124) in der Dissertation "Complete sequences of sets of integer powers" gestellt wurde, ist es noch niemandem gelungen, es zu lösen.

Der Kern von E124 ist: Gegeben seien k natürliche Zahlen d_i ≥ 2. Wenn ∑ 1/(d_i - 1) ≥ 1, dann existiert für jede natürliche Zahl n immer ein a_i, so dass n = ∑ a_i.

Und jedes a_i hat in Bezug auf d_i nur "Ziffern" aus der Menge {0,1}.

Einfach ausgedrückt, fragt es im Wesentlichen, ob man unter extremen Einschränkungen jede beliebig große Zahl immer in "Binärform" darstellen kann, unabhängig von der Basis?

Dies betrifft die "tiefe Zone" der Kombinatorik, und die traditionellen Methoden scheiterten an der gcd-Bedingung und an Randfällen.

Bis letzte Nacht fiel diese Mauer.

Das Harmonic-Team hat einen Prototypen einer "mathematischen Superintelligenz" namens "Aristoteles" entwickelt, der eine Kombination aus verstärkendem Lernen, Monte-Carlo-Baumsuche und der Lean-Formalisierungssprache ist.

Nachdem das Problem eingegeben wurde, hat es über eine Milliarde Beweisstrategien durchsucht und schließlich einen 100% überprüfbaren Satz ausgegeben.

Der Mathematiker Boris Alexeev hat gesagt, dass dies sein Lieblingssatz unter den drei von der KI ausgegebenen Sätzen ist:

theorem erdos_124 : ∀ k, ∀ d : Fin k → ℕ, (∀ i, 2 ≤ d i) → 1 ≤ ∑ i : Fin k, (1 : ℚ) / (d i - 1) → ∀ n, ∃ a : Fin k → ℕ, ∀ i, ((d i).digits (a i)).toFinset ⊆ {0, 1} ∧ n = ∑ i, a i

Adresse: https://github.com/plby/lean-proofs/blob/main/ErdosProblems/Erdos124.md

Übrigens gibt es das E124-Problem in zwei verschiedenen Versionen, beide von Erdős gestellt.

Derzeit hat die KI "Aristoteles" die einfachere Version gelöst.

In Bezug auf die Zeit hat Aristotle sechs Stunden gebraucht, während Lean nur eine Minute benötigte.

Der Betreiber der Erdős-Problem-Website hat gesagt, dass die Leistung von Aristotle am beeindruckendsten ist!

ChatGPT und Gemini haben fehlgeschlagen

Terence Tao hat dazu kommentiert: "Soweit ich weiß, haben die tiefgreifenden Forschungswerkzeuge von Gemini und ChatGPT keine neuen, wertvollen Literaturhinweise zu diesem Problem gefunden."

Gemini hat eine einfache Beobachtung gemacht: Wenn man die Zahl 1 ausschließt, wird die gcd-Bedingung notwendig. Es hat auch die Bedeutung der Bedingung erklärt

und sie mit einigen parallelen Forschungen über Cantor-Mengen in Verbindung gebracht, insbesondere mit dem "Newhouse gap lemma".

Allerdings hat es keine neuen Literaturhinweise, die direkt mit diesem Problem verbunden sind, gefunden.

ChatGPT hat sich stark auf diese Website als Hauptquelle verlassen, z.B. indem es den Beweis von Aristotle, andere Dissertationen, die auf dieser Seite zitiert werden, und die Seiten zu verwandten Problemen zitiert hat.

Daher hat es keine neuen Informationen erhalten, aber die von der KI generierten Zusammenfassungen können für die Leser dennoch interessant sein.

Terence Tao: Die KI erntet die "niedrigen Früchte" der Mathematik

Auf mathstodon hat Terence Tao auch seine Erfahrungen über die Jahre geteilt -

Er hat gesagt, dass die aktuelle Realität ist: Die ungelösten mathematischen Probleme folgen einer "langschwänzigen Verteilung", und die automatisierte "Ernte" durch die KI konzentriert sich genau auf das Ende der langen Schwanzes.

Es gibt eine große Anzahl von Problemen, die relativ einfach zu beweisen oder zu widerlegen sind, aber aufgrund der begrenzten Anzahl von Mathematikern, die sich wirklich mit der Forschung befassen können, haben diese Probleme fast keine Beachtung erhalten.

Mit anderen Worten, in diesem "Schwanz" verstecken sich viele "niedrige Früchte", die leicht zu erreichen sind:

Wenn es eine Möglichkeit gibt, diese Probleme in großem Maßstab automatisch zu lösen, könnte dies eine beträchtliche Anzahl neuer mathematischer Ergebnisse hervorbringen.

Letztes Jahr hat Terence Tao in einem ähnlichen Fall im Equational Theories Project mitgewirkt.

In diesem Projekt standen sie vor 22 Millionen möglichen Implikationen in der Allgemeinen Algebra. Wenn alles von Menschen gemacht werden würde, würde es sicherlich sehr viel Zeit in Anspruch nehmen.

Daher haben sie beschlossen, von Anfang an mit einem relativ "technikarmen" automatisierten Verfahren anzufangen und haben in nur wenigen Tagen die meisten Probleme gelöst.

Dann haben sie immer komplexere Methoden angewandt, um die hartnäckigen Probleme, die in den ersten Runden nicht gelöst werden konnten, zu lösen.

Am Ende haben es die menschlichen Mathematiker noch einige Monate gebraucht, um die letzten wenigen besonders hartnäckigen Probleme zu lösen.

Derzeit enthält die Erdős-Problem-Website 1108 Probleme, die in mindestens einer Dissertation von Erdős aufgetreten sind.

Darunter gibt es sowohl berüchtigte Probleme wie E3 als auch eine große Anzahl von weniger bemerkenswerten Problemen, die fast niemandem Beachtung geschenkt wurde, und sogar Erdős selbst hat sie nicht erneut untersucht.

In den letzten Wochen sind fast zehn "ungelöste" Markierungen auf dieser Website verschwunden, alle wurden bei der Literaturrecherche mit KI-Unterstützung entdeckt -

Tatsächlich wurden diese Probleme bereits von anderen gelöst.

Die menschlichen Mathematiker, die sich derzeit mit diesen Problemen befassen, verwenden auch KI-Werkzeuge und formale Beweishilfen:

Einige überprüfen bestehende Beweise in Lean, andere generieren Ganzzahlfolgen, die mit diesen Problemen verbunden sind, und wieder andere ergänzen fehlende Beweisschritte in einem bestehenden Ansatz.

Kürzlich wurde eine weitere Art von "niedrigen Früchten" entdeckt, die in den Bereich der Fähigkeiten der automatisierten Werkzeuge fällt - Probleme, die aufgrund technischer Mängel in der Beschreibung überraschend einfach zu lösen sind.

E124 ist ein typisches Beispiel. Die vollständige Version dieses Problems ist etwas schwieriger und ist in drei Dissertationen von Erdős aufgetreten.

Aber in zwei von ihnen fehlte eine Schlüsselannahme, so dass diese Version eigentlich nur eine direkte Folge des Brown-Kriteriums ist.

Dies wurde niemandem aufgefallen, bis Boris Alexeev das Problem an das automatische Werkzeug Aristotle weitergeleitet hat. Überraschenderweise hat die KI in wenigen Stunden selbständig die Lücke entdeckt und mit Lean einen formalen Beweis erbracht.

Man kann sehen, dass die KI das