KI-gestützter Beweisversuch der Collatz-Vermutung in Lean fehlgeschlagen
Ein KI-gestützter Versuch, die Collatz-Vermutung mit dem Lean-System zu beweisen, wurde als ungültig eingestuft. Eine kritische Schwachstelle in Lean 4.32.2 wurde schnell behoben.
Das Tech-Medium Gigazine berichtete, dass ein KI-gestützter Versuch, die Collatz-Vermutung zu widerlegen, gescheitert ist. Der Beweis, der im formalen Verifikationssystem Lean durchgeführt wurde, erwies sich als fehlerhaft, nachdem Experten ein signifikantes Problem im System selbst identifiziert hatten.
Die Collatz-Vermutung, auch bekannt als das 3n+1-Problem, ist ein notorisch einfaches, aber ungelöstes mathematisches Rätsel. Sie besagt, dass jede positive ganze Zahl schließlich die 1 erreicht, wenn sie einem bestimmten iterativen Prozess unterzogen wird: Ist die Zahl gerade, wird sie durch zwei geteilt; ist sie ungerade, wird sie mit drei multipliziert und eins addiert.
Ursprünglich kündigte Ramana Kumar am 25. Juli auf GitHub an, einen Weg gefunden zu haben, die Existenz von Zahlen zu beweisen, die nicht die 1 erreichen. Er nutzte das Lean-System, das die Korrektheit mathematischer Beweise programmatisch verifiziert. Kumars Behauptung war, dass sein KI-gestützter Beweis dies zeigte.
Später wurde bekannt, dass die von Kumar verwendete Methode es dem Lean-System erlaubte, fehlerhafte Aussagen zu akzeptieren. Der Forscher Kiran Gopinathan reduzierte das Problem auf einen kleineren, reproduzierbaren Codeausschnitt und meldete ihn dem Lean-Entwicklungsteam am 28. Juli. Die Schwachstelle lag im Kern von Lean und bezog sich auf die Verarbeitung von "verschachtelten induktiven Typen", was dazu führte, dass bestimmte Parameter die Verifizierung umgingen. Der Lean-Entwickler Leonardo de Moura bestätigte, dass das Problem auf unvollständige Prüfungen in der Kernel-Implementierung zurückzuführen war.
Das Lean-Entwicklungsteam beheob den Fehler umgehend. Ungefähr eine Stunde nach der Meldung veröffentlichte das Team am 28. Juli eine korrigierte Version, Lean 4.32.2, die die Integrität des Systems wiederherstellte. Obwohl der Versuch, die Vermutung zu widerlegen, scheiterte, stellt diese Korrektur sicher, dass das Lean-System ein zuverlässiges Werkzeug für die mathematische Forschung bleibt.