Collatz-Widerlegung entpuppt sich als Bug im Lean-Kernel
Why is it all in the kernel?
Ramana Kumar hat angeblich die Collatz-Vermutung widerlegt, doch der Beweis beruhte auf einem Fehler im Lean-Kernel, den auch der unabhängige Prüfer Nanoda übersah. Dieser Vorfall zeigt, dass Beweisobjekte keine Garantie für Korrektheit bieten. Der Autor argumentiert, dass der Ansatz, alles in den Kernel zu legen, unnötig ist: In einfachen Typentheorien lassen sich rekursive Definitionen durch ehrliche Arbeit außerhalb des Kerns konstruieren, wie Isabelle/HOL zeigt. Systeme wie HOL Light oder HOL4 sind daher sicherer.
Es ist ironisch, dass Beweisobjekte manchmal als Garant für größere Korrektheit angepriesen werden – das Gegenteil ist klar der Fall.