#Lean
共 4 篇
11 个正方形怎么摆最省：一份能被机器复查的证明
一份 Lean 4 仓库宣称完成了 11 个单位正方形最优装箱的无条件证明，边长约 3.87708。读完能看清它证了什么、信任边界在哪，以及怎么自己跑一遍验证。
数学家：OpenAI 没读懂自己那道证明
OpenAI 9 月公布 166 页纳维-斯托克斯证明，称沿用了两位西班牙数学家的路线。一个月后多组专家说并非如此。这篇讲清「结论可验证」和「作者讲得清」为什么是两件事。
Hales：Lean 查得出推导错，查不出你问错问题
2026 年夏天 Lean 内核连续爆出可靠性漏洞，有人借此"证明"了 Collatz 猜想的反例。读完能分清形式化验证保证了什么、没保证什么，以及为什么还要人工审计。
OpenAI 公开 AI 做数学的结果，附 Lean 证明
OpenAI 把内部前沿模型做出的数学结果放到 GitHub，附上可机器验证的 Lean 证明，还公开了 10 份推理摘要。读完你能分清哪些是可以检查的成果，哪些只是新闻标题里的说法。