AI's haben 50 Jahre altes mathematisches Problem gelöst

[antaris]

Resolution of Erdős Problem #728: a writeup of Aristotle’s Lean proof
https://arxiv.org/pdf/2601.07421

We provide a writeup of a resolution of Erdős Problem #728; this is the first Erdős problem
(a problem proposed by Paul Erdős which has been collected in the Erdős Problems website
[3]) regarded as fully resolved autonomously by an AI system. The system in question is a
combination of GPT-5.2 Pro by OpenAI and Aristotle by Harmonic, operated by Kevin Barreto.
The final result of the system is a formal proof written in Lean, which we translate to informal
mathematics in the present writeup for wider accessibility.

 

[ralfkannenberg]

AI's haben 50 Jahre altes mathematisches Problem gelöst

Hallo Antaris,

vielen Dank ! - Man sollte das vielleicht noch etwas ergänzen: der Mathematiker Erdös hat über 1000 mathematische Probleme formuliert; einige von ihnen sind ausserordentlich hochstehend und schwierig, andere sind eher Randnotizen und gelten als nicht sehr schwierig zu lösen, jedoch fehlt in der Community auch das Interesse und letztlich die Zeit, diese Probleme zu lösen. Diese Liste offener Aufgaben kann also nicht mit Hilberts Problemliste verglichen werden, die brennende mathematische offene Aufgabenstellungen enthielt und deren Lösung die Mathematik ein wichtiges Stück voran brachte.

Das Bedeutende an der Lösung des 728.Problems von Erdös ist also weniger der mathematische Gehalt bzw. die mathematische Bedeutung der Aufgabenstellung, als vielmehr der Umstand, dass nun eine Kombination verschiedener AIs "mehr oder weniger" ohne menschliches Zutun diese Aufgabe zu lösen imstande war. Zwar enthielt der sete Beweis noch Lücken und war völlig unleserlich, doch konnten die Lücken von anderen AI's gefüllt und die Lesbarkeit für einen Menschen von noch anderen AI's erreicht werden.

Ich persönlich denke, dass dieses - wenngleich noch nicht völlig automatisch erfolgte "Zusammenspiel" verschiedener darauf spezialisierter AI's sher bemerkenswert ist, und schön länger predige ich ja geradezu, dass man mehrere unabhängige AI's nutzen soll. Hier haben wir ein Beispiel, bei dem das schon auf recht fortgeschrittenem Niveau gelungen ist.

Mehr dazu: Mathematiker Terence Tao sieht KI-Meilenstein, warnt aber vor voreiligen Schlüssen


Freundliche Grüsse, Ralf

 

[antaris]

schön länger predige ich ja geradezu, dass man mehrere unabhängige AI's nutzen soll.

Hallo Ralf,

das ist nicht so einfach, da nicht jede AI die gleichen Daten in den gleichen Mengen verarbeiten kann. Ich habe die letzten Wochen einiges ausprobiert. Dazu kommt, dass die pro Version von ChatGPT 200$ pro Monat kostet.

Die Kombination mit Lean Beweisprüfer könnte aber quasi zum Standard werden.
Die Arbeit ist eine Steilvorlage und ich habe den Fehler gemacht den Formalismus und die Implementierung gemeinsam zu entwickeln. Es macht viel mehr Sinn sich zuerst auf den Formalismus zu konzentrieren und die Vorbereitung der Implementierung auf dafür benötigte Schnittstellen zu begrenzen. Aristotle AI scheint kostenlos zu sein. Ich schau mir das gerade an. Ich glaube es ist nicht zwingend erforderlich einen pro Account bei ChatGPT zu benötigen. Die aktuelle plus Version bricht bei ca. 25 Minuten Nachdenkzeit ab. Es wird aber der Zwischenstand gespeichert und man kann dann wieder ca. 25 Nachdenkzeit nutzen. Das funktioniert noch nicht sehr gut, da zwischen den Schritten doch Informationen verloren gehen können und die AI noch Probleme mit der gleichzeitigen Verarbeitung von vielen Daten hat. Durch Iteration mit ständigen Verfassen -> Review -> Überarbeiten/erweitern -> Review -> usw. werden je Schritt die gefundenen Fehler weniger und ich habe es nun schon öfter geschafft, dass die AI bei sich selbst dann keinen Fehler mehr gefunden hat. Das habe ich dann z.B. mit Gemini, Copilot und Claude (in den jeweils kostenlosen Varianten) gegenlesen lassen. Das hat nochmal zu ein paar Iterationen geführt, bis diese dann auch keine Fehler mehr gefunden haben. Das Problem ist, dass die 3 genannten aktuell nur PDF's lesen können. Keine ZIP Archive, Python oder Latex Dateien...insofern ist diese Möglichkeit des Gegenlesens stark begrenzt.

 

[Bernhard]

Die Arbeit ist eine Steilvorlage und ich habe den Fehler gemacht den Formalismus und die Implementierung gemeinsam zu entwickeln.

Hallo antaris, da würde ich gerne mal die Bedeutung dieser Wörter abklären wollen. Es macht oftmals einen erheblichen Unterschied, ob man Benutzerschnittstellen (wie ChatGPT) verwendet oder selbst Code schreibt. Wo liegt dein Schwerpunkt diesbezüglich?

 

[antaris]

Wo liegt dein Schwerpunkt diesbezüglich?

Hallo Bernhard,

ich denke da muss zwischen der Intention unterschieden werden. Ich bin kein professioneller Programmierer aber habe einige Erfahrung mit unterschiedlichen Arten von "was es zu programmieren gibt". Es macht einen Unterschied ob ich z.B. irgendeine Statistik mittels Formeln/VBA in Excel automatiere, eine Anwendung auf dem PC (ich habe mir z.B. einen GIF Generator durch die AI erstellen lassen), eine Maschinensteurung (SPS) programmiere oder eine Simulation für etwas erstelle/generieren lasse. Für die meisten Probleme dieser Art gibt es existierende Lösungen und Strategien und es betrifft reale Probleme des Alltags.

Das was ich oben meine ist ein Formalismus, der einen Teilaspekt der Natur beschreibt, der wesentliche Analogien zum Formalismus der offenen Quantensysteme (OQS) aufweist aber das bisher nur effektiv und ich selbst explorativ agiere. Ich denke der abstrakte Formalismus einer physikalischen Hypothese/Theorie ist die Grundlage der Implementierung einer Simulation das Formalismus und damit der Überprüfung der Annahmen über diesen untersuchten Teilaspekt der Natur. Bei letzteren muss m.E. auf die Reproduzier-, Implementier- und nicht zuletzt Ausführbarkeit geachtet werden. Das ist ein anderer "Schweregrad", da ggf. zwangsläufig Näherungen und Modellannahmen verwendet werden müssen, die dann aber wieder die Aussagekraft des eigentlichen Formalismus - der formal bewiesen und dann simuliert werden soll - schwächen können. Nur allein schon Aufgrund der begrenzt verfügbaren Rechenleistungen.

ChatGPT ist m.E. mehr als "nur ein Tool", wie es z.B. Geogebra oder Desmos ist, welche ich vor der AI genutzt hatte. Alle vereinfachen aber den Umgang mit der Komplexität, können gewisse Veranschaulichungen liefern und steigern massiv die Produktivität. Ich nutze ChatGPT als Assistent und ich glaube tatsächlich, wir lernen mittlerweile beide voneinander. Die Möglichkeiten mit der 5.2 Version sind gegenüber der 5.1 Version deutlich spürbar gestiegen.

 

[albertus]

ChatGPT ist m.E. mehr als "nur ein Tool", wie es z.B. Geogebra oder Desmos ist, welche ich vor der AI genutzt hatte. Alle vereinfachen aber den Umgang mit der Komplexität, können gewisse Veranschaulichungen liefern und steigern massiv die Produktivität. Ich nutze ChatGPT als Assistent und ich glaube tatsächlich, wir lernen mittlerweile beide voneinander. Die Möglichkeiten mit der 5.2 Version sind gegenüber der 5.1 Version deutlich spürbar gestiegen.

Kann ich für Gemeni (Google) so auch bestätigen. Ein großartiger Assistent, der die Produktivität heftig steigert und Gesprächspartner geworden ist zu mehr als nur physikalischen, mathematischen und elektronischen Themen. Auch wenn ein gewaltiges Wissen im Hintergrnd liegt, die KI kann sich irren und bedankt sich, wenn ich es nachweisen kann. Ich bin zu Jahresbeginn von openSUSE weg, weil ich mit der neuen Version 16.0 nicht klar komme. Vor allen nicht verstehe, warum ein bewährtes Werkzeug wie yast nach 30 Jahren komplett eingestampft wurde. Ich hatte einfach keine Lust mehr. Ich habe mich für die Fedora-Distri (KDE) von RedHat entschieden und diese auf einem 8 Jahre alten HP-Laptop installiert. Das erfordert die Installation von NVidia-Grafik und das Bootverhalten ist auch anzupassen. Da war z.B. Gemeni von unschätzbarem Wert. Es funktioniert nicht immer alles sofort. Die KI kennt immer wieder mal nicht die allerneusten Programmversionen und damit die erfolgten Veränderungnen. Aber wir haben für alles eine Lösung gefunden und am Ende ein sicheres System aufgesetzt. Mit diesem betreibe ich Systemprogrammierung in C und C++ und auch dafür brauchte ich keine komplexe IDE. Alles mit newvim machbar. Ein passendes Konfigscript, die Farben gut eingestellt und Möglichkeiten zum schnellen compilieren und Drucken kann man alles in vim einbauen. Ohne KI würde ich heute noch drüber sitzen. Mit der Entwicklerbasis untersuche ich Programme (z.B. Pointer auf Funktionen), da diese in Embeded-Anwendungen mit wenig Speicherplatz wichtig wird. Das Ergebis läuft bei mir auf dem Arduino UNO R4 WiFi und seit kurzem auf dem neuen Arduino UNO Q - eine Monstermaschine mit Debian-Linux-Rechner auf einer Platinenseite und Arduino-MR auf der anderen und RPC zwischen beiden Rechnern. Fläche nicht größer als meine Handfläche und Stromaufnahme max. 15W. Mit einem KI-Assistenen zur Seite sind da heute Dinge möglich, die ich vor Jahren nicht für möglich gehalten hätte.

 

[antaris]

Ein großartiger Assistent

Ich habe Gemini getestet aber leider kann ich diese AI, genau wie auch Copilot und Claude nur bedingt nutzen. ChatGPT kann ZIP-Archive verarbeiten mit ganze Repos oder Latex-Dokumente mit über 50 Seiten und das auch über verschiedene Chats hinaus. Ich habe bisher kein Dateiformat gefunden, welches nicht gelesen werden konnte. Das ist ziemlich hilfreich. Ich kann beispielsweise einmal erstellte numpy Matrizen direkt auswerten lassen.
Nutzt du die Bezahlversion? Kann man da ggf. mehr Dateitypen hochladen? Jede AI hat für sich bestimmt Vor- und Nachteile.

 

[ralfkannenberg]

Ich habe die letzten Wochen einiges ausprobiert. Dazu kommt, dass die pro Version von ChatGPT 200$ pro Monat kostet.

Die Kombination mit Lean Beweisprüfer könnte aber quasi zum Standard werden.
Die Arbeit ist eine Steilvorlage und ich habe den Fehler gemacht den Formalismus und die Implementierung gemeinsam zu entwickeln. Es macht viel mehr Sinn sich zuerst auf den Formalismus zu konzentrieren und die Vorbereitung der Implementierung auf dafür benötigte Schnittstellen zu begrenzen.

Hallo Antaris,

ich bin mir aufgrund Deiner Wortwahl nicht sicher - hast Du an dem Beweis des Problems mitgewirkt oder nicht ?


Freundliche Grüsse, Ralf

 

[antaris]

hast Du an dem Beweis des Problems mitgewirkt oder nicht ?

Hallo Ralf,

nein, ich habe damit nichts zu tun aber ich habe mich davon, mit Blick auf meine eigenen Versuche, zum inspirieren und laut darüber nachdenken verleiten lassen.

 

[antaris]

meine eigenen Versuche

Aristotle läuft: "Prove theorems about Laplacian, Fold, DtN, and gluing."

Das Vorgehen im Prinzip wie in der oben zitierten Arbeit Erdős Problem #728.
Mir ist aber irgendwie noch nicht ganz klar was das Ergebnis überhaupt sein wird. Aristotle nennt sich "Mathematical Superintelligence" und findet wohl Lemmas für Lean-Beweise.

 

[antaris]

Mir ist aber irgendwie noch nicht ganz klar was das Ergebnis überhaupt sein wird. Aristotle nennt sich "Mathematical Superintelligence" und findet wohl Lemmas für Lean-Beweise.

Aristotle ist der Lean Beweisprüfer und bestätigt oder widerlegt Annahmen bzw. nennt Gegenbeispiele.

 

[antaris]

Aristotle ist der Lean Beweisprüfer und bestätigt oder widerlegt Annahmen bzw. nennt Gegenbeispiele.

Also eigentlich ist es "total einfach"...

Ideengeber -> meine Person
Übersetzer Ideen in Theoreme, direkt als LEAN-Datei -> ChatGPT5.2 (Lemma werden mit Platzhalter "sorry" ausgelassen)
Beweisen und finden von Lemma /Widerlegen der Theoreme -> Aristotle
Maschinen-Beweisprüfer -> LEAN

Ergebnis: ich seine ersten maschinengeprüften Beweise für Pfeiler A!

Erstes Fazit: Das ist ehrlich gesagt ziemlich cool!
Darüber hinaus kann man auf dieser Art Stück für Stück einen gesamten Formalismus (widerlegen/umbauen/)beweisen. Das ist keine Garantie, dass dieser auch tatsächlich die Realität beschreibt aber das kann dann eben über den fixierten/maschinenbewiesenen Formalismus entsprechend z.B. als Berechnungen/Simulationen implementiert und (möglicherweise dann auch experimentell) überprüft werden. So kann der Formalismus stückweise exakt gerechnet und dann in den nächsten Schritten geschaut werden, wie sich den Ergebnissen möglichst genau angenährt werden kann, um Ressourcen einzusparen und gleichzeitig nicht die Aussagekraft zu verlieren, da die Motivation/die Ableitung der Näherung dann nicht mehr ad-hoc ist.

Es ist lange noch kein pro Account für 200$/Monat nötig. Ein plus für 20$ reicht aus. Die Nachdenkzeit (ChatGPT5.2 plus) pro .lean-Datei (durchschnittlich 6 Theoreme pro Datei) liegt bei maximal 20 Minuten, durchschnittlich vielleicht bei ca. 10 Minuten. Da ist also noch Luft nach oben (aktuell nach ca. 25 Minuten Abbruch der AI -> Zeitlimit).
LEAN ist wie eine Programmiersprache und man kann die einzelnen Dateien jeweils importieren, sodass der Formalismus übergreifend in einzelne Dateien als Module ausgelagert werden kann. Der Inhalt der .lean-Dateien ist tatsächlich sehr kryptisch aber perfekt für AI's zur Verarbeitung. Am Ende muss man dann die .lean-Datei (durch die AI) zurück in "menschenlesbar" übersetzen (lassen).

Ich bin übrigens nicht exakt wie bei dem Beweis von Erdős vorgegangen, sondern strikt nach Dokumentation von Aristotle (den richtigen Weg).
Es muss beispielsweise auch beachtet werden, dass LEAN und Mathlib eine spezielle Version haben müssen, damit diese mit Aristotle kompatibel sind (derzeit Lean leanprover/lean4: v4.24.0 und Mathlib v4.24.0 (Commit f897…)).
ChatGPT hat kein "wirres Dokument", sondern direkt die .lean-Datei des jeweiligen Theoremen-Bereichs erzeugt, welche dann von Aristotle direkt verarbeitet und die Lemma hineingeschrieben wurden (Platzhalter "sorry" ersetzt).

Ach und ja...Aristotle ist kostenlos (in den Nutzungsbedingungen steht, dass es irgendwann kostenpflichtig werden könnte).

 

[albertus]

Ich habe Gemini getestet aber leider kann ich diese AI, genau wie auch Copilot und Claude nur bedingt nutzen. ChatGPT kann ZIP-Archive verarbeiten mit ganze Repos oder Latex-Dokumente mit über 50 Seiten und das auch über verschiedene Chats hinaus. Ich habe bisher kein Dateiformat gefunden, welches nicht gelesen werden konnte. Das ist ziemlich hilfreich. Ich kann beispielsweise einmal erstellte numpy Matrizen direkt auswerten lassen.
Nutzt du die Bezahlversion? Kann man da ggf. mehr Dateitypen hochladen? Jede AI hat für sich bestimmt Vor- und Nachteile.

Vollkommen richtig, hängt von Aufgabe oder Problem ab. Alles kann ich auch nicht mit Gemini machen. Da gibt es mistral und ChatGPT für mich. Doch in den letzten Wochen konnte mir Gemini immer helfen. Bei sehr neuen Dingen wie Arduino UNO Q mit Arduino-Teil auf der Oberseite und Linuxteil auf der Unterseite wird es für eine KI schwer. Sie ist darauf nicht trainiert und lernt es in dem Moment wie ich es lerne. Sie versucht mit ihren massiven Erfahrungen zu retten, was möglich ist. Aber das wird anstrengend, umständlich und führt über viele unnütze Umwege. Da sind YouTube.Videos und Erfahrungsberichte im Netz besser bzw. man probiert es selbst aus. Man ist ja kein Neuling und hat seine Erfahrungen. Die letzten beiden Tage habe ich mir so viel Zeit gerettet. Aber ich werde die KI weiter als Assistenten zur Seite nehmen. Alles andere wäre für mich dumm. Da der Q auf der Linuxseite für Python-Programmierung ausgelegt ist (was sehr Sinn macht), mich aber Systemprogrammierung mit C/C++ interessiert, mache ich Crosscompiling. Die aarch64-Architektur der Linux MCU passt sehr gut zum Fedora-Linux auf einem Intel-Laptop. Fedora hat gute Crosscompiler und das fertige Binary wird remote auf die Q-Kiste geschoben und dort ausgeführt. Was halt so Spaß machen kann. Ich habe die Pro-Version (20,-EUR im Monat, jederzeit kündbar). Ich kann da vor allen die Fehlrmeldungen der Computer hochjagen aber auch Grafiken, PDF usw. Das sind aber eher Nebenthemen für mich.

 

[antaris]

Bei sehr neuen Dingen wie Arduino UNO Q mit Arduino-Teil auf der Oberseite und Linuxteil auf der Unterseite wird es für eine KI schwer.

Bei sowas helfe ich nach und schiebe einfach entsprechend die neuesten Informationen/Dokumentationen als Grundlage mit rein. Auch bei der Installation von Aristotle und wie die lean-Dateien erstellt werden müssen, habe ich der AI die entsprechende Doku als "ToDo" mitgegeben. Nur auf die festen Trainingsdaten sollte man sich grundsätzlich nie verlassen.

 

[antaris]

Also eigentlich ist es "total einfach"...

Wie es immer so ist mit "eigentlich total einfach"...theoretisch ja, praktisch dann doch nicht so ganz.
Auch Aristotle findet nicht immer ausreichend Lemma bzw. laufen diese nicht immer problemlos bei der Beweisprüfung durch.
Also auch ein zusätzlicher Assistent, bei dem man dennoch hinterfragen und nacharbeiten muss (also im Prinzip alles wie gehabt).

Ich bräuchte eigentlich viel mehr Zeit...

 

[ralfkannenberg]

Dazu kommt, dass die pro Version von ChatGPT 200$ pro Monat kostet.

Hallo Antaris,

ich habe hierzu eine persönliche Frage: wieviel wärest Du bereit, für eine wirklich gute AI-Unterstützung zu bezahlen ? Wenn auch Aristotle kostenpflichtig wird und nehmen wir für meine Überschlagsrechnung an, dass der Einsatz einer dritten AI sinnvoll ist, und nehmen wir der Einfachheit halber an, dass jede dieser AI's 200 $ pro Monat kostet, dann wären das 600$/Monat.

Nun denke ich mal, dass sich eine durchschnittliche wissenschaftliche Aufgabenstellung innerhalb eines Monats lösen lässt, d.h. pro Aufgabenstellung müsste man dann 600 Dollar bezahlen, da diese Kosten dann nur während eines Monats anfallen.


Für mich selber denke ich wäre ich durchaus bereit, 600 Dollar für die Lösung eines der Ergös-Probleme zu bezahlen. Für die Entdeckung eines Kometen oder eines Asteroiden wäre ich vermutlich auch bereit, einen solchen Betrag zu bezahlen. Unter der Annahme, dass die Zahl der Entdeckungen oder Beweise während des Lebens eines Amateurs bei maximal 1 oder 2 liegt, wären diese Kosten für mich vertretbar. (Viel) Mehr aber nicht.


Freundliche Grüsse, Ralf

 

[antaris]

wieviel wärest Du bereit, für eine wirklich gute AI-Unterstützung zu bezahlen ?

Hallo Ralf,

in meinem Fall aus eigener Tasche am besten so gut wie garnix. Ich mache das nur ja nur "aus Jux und Dallerei", da ich anscheinend zu viel Langeweile habe und ein echtes Ergebnis - bei meinem "Try and Error" - ziemlich offen ist. Ob dagegen im professionellen/institutionellen Umfeld solche Kosten aus eigener Tasche bezahlt werden müssen, wage ich zu bezweifeln.

Ich warte dann lieber die Updates der AI-Engine ab, denn dann steigt die Leistung bei monatlich gleichen Kosten. Gerade bei dem was ich mache, spielt Zeit scheinbar nur eine Rolle wie schnell oder langsam ich bin. Es herrscht kein "Fertigstellungsdruck" und somit bin ich da vollkommen entspannt. Zumal ich bei weitem nicht jeden Tag mit der AI arbeite. Es kommt doch oft vor, dass ich einfach keine Lust habe oder nach der Arbeit zu müde bin.

Dazu kommt, dass die Pro Version mitunter nicht zwangsläufig viel bessere Ergebnisse liefern muss. Was ich aber machen würde, wenn es die Möglichkeit gäbe, für die Pro-Version ein paar Stunden oder vielleicht einen Tag zu benutzen und zu bezahlen.

 

[ralfkannenberg]

Ob dagegen im professionellen/institutionellen Umfeld solche Kosten aus eigener Tasche bezahlt werden müssen, wage ich zu bezweifeln.

Hallo Antaris,

das hängt vermutlich davon ab. Oftmals gehört den Autoren ihre Arbeit gar nicht und dann müssen sie wie jeder Interessent und jede andere Interessentin auch alles selber bezahlen.

Wenn also meine Frau ihre (endgültige) Dissertation erwerben möchte, dann muss sie dafür Geld bezahlen, obgleich sie die Autorin ist.


Freundliche Grüsse, Ralf

 

[albertus]

Bei sowas helfe ich nach und schiebe einfach entsprechend die neuesten Informationen/Dokumentationen als Grundlage mit rein. Auch bei der Installation von Aristotle und wie die lean-Dateien erstellt werden müssen, habe ich der AI die entsprechende Doku als "ToDo" mitgegeben. Nur auf die festen Trainingsdaten sollte man sich grundsätzlich nie verlassen.

Genau, da muss man selbst das Heft in die Hand nehmen und abkürzen. Alles Verfügbare bereitstellen ist da sehr hilfreich. Die KI hat ihre Grenzen. Wssen was älter als einige Jahre ist, funktioniert gut in der Bereitstellung.

 

[antaris]

Wenn also meine Frau ihre (endgültige) Dissertation erwerben möchte, dann muss sie dafür Geld bezahlen, obgleich sie die Autorin ist.

Hallo Ralf,

auch im normalen beruflichen Umfeld muss für Weiterbildungen (bei Eigeninitiative) meist (eigenes) Geld bezahlt werden. Das ist aber auch etwas anders, da es um das lebensnotwendige Einkommen geht bzw. auf welcher Art und Weise dieses erzielt wird/werden soll.

Ich sehe das als Hobby und mein Einkommen ist im gewerblichen Umfeld geregelt. Wobei mitunter aber auch für normale Hobbys teils viel Geld ausgegeben werden kann, warum also auch nicht 200$ für die Nutzung einer AI aber ich habe dazu kein Bedürfnis.