Bug de sonido en el kernel de Lean: una prueba falsa de Collatz expone una falla crítica

Postmortem for Kernel Soundness Bug #14576

Un error de solidez en el kernel de Lean permitió una 'refutación' falsa de la conjetura de Collatz, generada con IA. El bug, que afecta a los tipos inductivos anidados, fue reportado y corregido en una hora. El problema solo es explotable mediante metaprogramación y no afecta la meta-teoría. Además, se descubrió un error independiente en nanoda, el verificador externo en Rust. Se han añadido pruebas de regresión y se ha reforzado el kernel.