共 2 篇
一份 Lean 4 仓库宣称完成了 11 个单位正方形最优装箱的无条件证明，边长约 3.87708。读完能看清它证了什么、信任边界在哪，以及怎么自己跑一遍验证。
2026 年夏天 Lean 内核连续爆出可靠性漏洞，有人借此"证明"了 Collatz 猜想的反例。读完能分清形式化验证保证了什么、没保证什么，以及为什么还要人工审计。