Lean 内核被 AI 攻破之后：v4.35.0 带上五个证明内核，两个完成形式化验证AI 生成的数学证明能不能信，取决于最后把关的验证器本身有多可靠。10 月 15 日发布的 Lean v4.35.0 给这个问题一个工程答案：这个定理证明器现在自带五个证明内核，其中两个是经过形式化验证的，一条命令就能让它们交叉复检同一批证明。 leanprover/con-leche：带一致性证明的外部 Lean 检查器 Lean 是当下 AI 数学生态的…2026/10/18开源AI安全形式化验证编程语言
十个 Claude 智能体写下 17895 行证明：汤姆逊问题 N=7 被 Lean 形式化验证了Vals AI 官方博客头图：五角双锥构型示意 2026 年 9 月 28 日，Vals AI 研究员 Hung Tran 发布了一项结果：十个 Claude Sonnet 5.5 智能体在约 15 小时内协作产出一份 17895 行的 Lean 4 形式化证明，证明对象是汤姆逊问题（Thomson problem）的 N=7 情形。证明通过了 Lean 内…2026/10/02AI智能体数学Lean形式化验证
AI 连破三大数学猜想：Jacobian 猜想 87 年反例与形式化验证的新时代AI 连破三大数学猜想：从反证法看 2026 年的形式化数学革命 2026 年 7 月 20 日，世界杯决赛正踢得胶着。数学家 Levent Alpöge 发了一条推文——Claude Fable 找到了 Jacobian 猜想的一个反例。87 年的公开问题，反例只有一行多项式。 同一天，剑桥数学家 Kevin Buzzard 在博客上写了一篇长文，标题是…2026/07/21开源AI数学Lean形式化验证
