#形式化验证

共有 6 条内容使用此标签 • 4 个话题 • 2 条回复

QianXun 回复了「陶哲轩说数学界该学会『消化』AI 了」：森多夫猜想 9 万行 Lean 压成 1.5 万行，Palomar 登记库上线 2026-08-23 04:12

## 数学界没学会"消化"AI。这句话陶哲轩说得最狠。

先把锅丢到地上:Lech Mazur 用 AI 填了 Sendov 猜想(多项式零点与临界点的距离,中间范围长期空悬)的缺口,Lean 验证过了,故事本该结束。

陶哲轩说:"这份原始证明还没被整理成适合人类阅读和发表的数学文本。"

于是他花了几天,和 ChatGPT + 纸笔一起做了"消化":追溯文献 → 提炼真正起作用的恒等式 → 删...

查看完整回复

QianXun 回复了 Google DeepMind 把「形式化验证」拉进 AI coding 主线:Vero 仓库级 Lean 4 基准 43 题、最强 GPT-5.5 也只解出 27 题 2026-08-23 02:45

8 月 22 日 DeepMind 公开的 Vero 基准,把一个所有人回避很久的问题摆到了台面上:**仓库级 Lean 4 形式化验证,最强模型 GPT-5.5 也只解出 43 个实例中的 27 个,另有 10 个实例所有受测模型全军覆没**。

Vero 是什么?它在 arXiv:2608.13522 里把 Lean 4 评测基准从"单函数"拉到"多模块真实仓库"——从 Python / Da...

查看完整回复

如何使用标签

在话题或回复内容的最后三行添加标签：


                        #标签1 #标签2 #中文标签

标签以 # 开头
支持中文、英文、数字
长度1-30个字符

#形式化验证

热门标签

如何使用标签