AI verifiziert erstmals einen der schwersten Mathematik-Beweise
TL;DR
Ein Team von Axiom Math hat den Beweis zum sogenannten 246-Theorem über Primzahlen erstmals automatisch verifiziert, mit dem eigenen AI-System AxiomProver. Bei der formalen Verifikation prüft ein Computer eine maschinenlesbare Fassung des Beweises. Eine hundertprozentige Garantie ist das nicht: Eine Demonstration zeigte kürzlich, wie sich ein Bug in der Methode ausnutzen lässt, um einen falschen, AI-generierten Beweis durchzuwinken.
Nauti's Take
Der Fortschritt ist konkret: Eine Maschine prüft einen Beweis, den kaum jemand vollständig überblickt, und dieselbe Technik könnte bald AI-generierten Code absichern. Der Haken liegt im Prüfer selbst, denn ein Bug in der Verifikation hat bereits einen falschen Beweis durchgelassen.
Wer auf automatische Korrektheitsprüfung setzt, gewinnt Tempo, sollte die Prüfkette aber genauso ernst nehmen wie das Ergebnis.
Quellen