La conjetura de Collatz refutada: un bug en el kernel de Lean
Why is it all in the kernel?
La conjetura de Collatz ha sido supuestamente refutada, pero la prueba resultó ser incorrecta debido a un bug en el kernel de Lean, que ni siquiera el verificador independiente Nanoda detectó. El autor reflexiona sobre la carga de los objetos de prueba y la filosofía de 'robo versus trabajo honesto' en los asistentes de demostración, defendiendo que los sistemas basados en teoría de tipos simples y teoría de conjuntos, como Isabelle/HOL, son más seguros al mantener las definiciones fuera del kernel.
La ironía es que a veces se promocionan los objetos de prueba como una garantía de mayor solidez. Lo contrario es claramente cierto.