标签
对 Lean 内核中一个可靠性漏洞的事后剖析，该漏洞被利用来产生考拉兹猜想的“反证”，并说明了修复方案以及为什么独立的检查器最初也未能发现它。
Lawrence Paulson 讨论了因 Lean 内核中的一个 bug 导致的 Collatz 猜想的虚假反驳，并对证明对象和证明助手的可靠性进行了思考。
一个由AI生成的Lean形式化证明声称推翻了Collatz猜想，实际上利用了Lean内核中的两个漏洞（现已修复）。Lean创始人Leo de Moura警告说，这种情况还会继续发生，因为AI非常擅长发现健全性漏洞。
一个经 Lean 验证的新形式定理表明，对于趋向无穷的阈值，几乎所有正整数都在 436 ln N 个 Collatz 步内降至该阈值以下，强化了陶哲轩先前的结果，并给出了显式界限和自然密度。
Unicode 的转写规则（UTS #35）通过编译2-标签系统被证明是图灵完备的，显示终止问题不可判定。这一结果影响了许多系统中使用的 ICU 库。