Dan Abramov beweist mit KI eine 50 Jahre alte Vermutung von John Conway
I Vibed a Proof of Conway's Conjecture
Der React-Entwickler Dan Abramov hat mit Claude und ChatGPT einen Lean-Beweis für Conways Verfeinerungsvermutung über omnifische ganze Zahlen erstellt. Ein Monat Freizeit und unzählige Tokens flossen in das Projekt, das der Palomar-Registry zur mechanischen Prüfung vorliegt. Die mathematische Fachwelt hat den Beweis noch nicht unabhängig verifiziert, doch Abramov lädt ausdrücklich zum Widerlegen ein und beschreibt offen, wie die Modelle zunächst in dramatischem Wortschwall versanken, bevor ein skeptischerer Ansatz brauchbare Teilergebnisse lieferte.
Ich hielt die Idee, ein Mathematikproblem zu „lösen“, ohne seine Substanz zu verstehen, für ziemlich absurd – was es natürlich nur umso verlockender machte.