Lean内核漏洞：Collatz猜想被误证

Why is it all in the kernel?

Ramana Kumar声称推翻了Collatz猜想，但证明因Lean内核的漏洞而无效，连独立检查器Nanoda也未能发现。这暴露了过度依赖证明对象（proof objects）的弊端：它们像拖在车后的备用轮胎，既增加负担，又在主车故障时同样失灵。作者Lawrence C. Paulson反思，现代证明助手为追求便利，将递归等复杂结构直接植入内核（即“盗窃”），而非通过基础公理严谨推导（即“诚实劳动”）。这种捷径虽能简化实现，却埋下了Soundness隐患。相比之下，坚持最小化内核的HOL Light或Candle系统更为稳健。