Lean-Kernel-Soundness-Bug: Beweis von False durch AI-generierten Collatz-Gegenbeweis

Postmortem for Kernel Soundness Bug #14576

Ein Soundness-Bug im Lean-Kernel (#14576) wurde entdeckt und behoben. Ramana Kumar veröffentlichte einen vermeintlichen Gegenbeweis zur Collatz-Vermutung, der einen Fehler in der Behandlung verschachtelter induktiver Typen ausnutzte. Der Bug war nur über Metaprogrammierung erreichbar und wurde von Kiran Gopinathan zu einem Beweis von False reduziert. Das Lean FRO veröffentlichte Fixes und verstärkte Kernel-Invarianten. nanoda, ein unabhängiger Checker, hatte einen separaten Bug, der ebenfalls behoben wurde. Die Verifikation mit lean4lean ist noch nicht abgeschlossen.