AI攻克数学与形式化验证
探讨AI在Lean等数学定理证明与形式化推理中的突破
2个信源参与该主题的先锋
全部段落
10月26日
- Alex Kontorovich 嘉宾称，AI 的数学能力突然跃升，令此前的预测不再可靠。 讨论涉及 OpenAI 一次发布的约 700 道题，以及据称包括 unique games 和 quasi-Riemann 在内的证明；Kontorovich 说，公开题集中包含数千道尝试题中的正向结果，表面成功率约为 10%。讨论中，完整的黎曼猜想和 P vs NP 仍未解决 …
- 形式化验证为 AI 的数学论断提供了可核验路径，但可复用的证明基础设施仍未建成。 Kontorovich 称，Anthropic 用约 1300 万行 Lean 形式化了费马大定理，但区分了经检查的结果，与能整洁、可维护地并入 Mathlib 的贡献。系统靠“临时拼凑”达到正确后，证明的整理、讲解和复用仍是大量工作。
- Steven Brunton 所谓 Navier–Stokes 突破，并未实质改变商业价值更高的流体设计问题。 Brunton 说，这是一个精心构造、受平滑外力驱动的三维爆破解，处于常规工程条件之外。他明确区分：“我们解决了 100 万美元的数学问题”，但预测和控制实际流动仍是横跨交通、国防、健康与能源的“1 万亿美元工程问题”。
- Lex Fridman Podcast 仅凭重新组合，AI 也可能改变一个研究领域。 Kontorovich 更认可“半群”这一说法：想法可以反复复合；他不认同把 AI 贬作在固定气球内插值。Moitra 举的具体例子，是一项与 Anthropic 有关的 3SUM 结果：更快的算法推翻一项难度假设，改变下游算法，并迫使研究者重新思考哪些问题应归为一类。
- Kevin Hartnett AI 数学正沿着形式化与自然语言两条路径推进。 Hartnett 对比了 AlphaProof 在 2024 年 IMO 上凭借 Lean 和大量算力取得的银牌水平成绩，以及 Google DeepMind 和 OpenAI 在 2025 年 7 月公布的、以自然语言作答的金牌水平成绩。模型生成大量候选证明时，Lean 仍能提 …
- Machine Learning Street Talk 形式化的成本相对其预期收益过高，一直是采用门槛。 Hales 花了 20 人年形式化 Kepler 猜想；de Bruijn 因子意味着每行非形式化文本往往要写 20 行或更多形式化代码。数学家最想做的是“发现新数学”，因此自动化和加深理解，比单靠确保正确性更能推动采用。
- 自动形式化把稀缺精力转向了数学库的设计与维护。 AI 将论文转成 Lean 的速度远快于人类团队，但经过检验的代码仍可能使用繁琐的定义和薄弱的抽象。Hartnett 称这股涌入“有点像特洛伊木马”；Buzzard 预计 AI 生成的数学库会越来越大，同时坚持 mathlib 必须守住概念质量。
- Kevin Buzzard 机器验证把信任问题向上游推到了定义和规格说明。 Buzzard 的团队形式化了 50 条 Annals 定理陈述，随后用 AI 找出翻译错误，以及涉及 4 位菲尔兹奖得主的已发表定理陈述中遗漏的假设。这些案例里，专家理解作者本意，但照字面写出的陈述并不成立：“显然，n 必须至少是 3。”
- Machine Learning Street Talk 形式化既能加深理解，也能推动新发现。 检查 Scholze 的 6 页论证，带来了概念上的简化，也化解了他对无人仔细读过该论证的担忧：“终于真的有人读过它了。”另一次合作中，Tao 把 2,200 万个蕴含关系问题缩减到只剩 4 个未解案例，同时发现了此前陌生的数学构造。
10月19日
10月15日
10月10日
- David Sacks OpenAI 发布700多篇论文、370项据称的成果，展示了数字化可验证工作的经济学。 Friedberg 称这可能是“人类历史上最伟大的发现日”：据报道，每项证明平均只需不到3小时算力，因为数学猜想、测试和修正都可以并行、在数字环境中完成。Sacks 将这一判断延伸到编程领域：编译器提供了同样廉价、客观的反馈闭环。
- 这些数学结果更有力地证明了机器正在获得推理能力，而非人类福祉即将迎来现实突破；但嘉宾甚至对这一区分本身存在分歧。 Friedberg 提到芯片优化、矩阵乘法、量子传感器和密码学研究的潜在影响；Chamath 则认为，许多问题只是“非常小、非常狭窄”的知识死胡同，并非被物理学长期卡住的前沿。Friedberg 还指出，关于缺失的密码学论文和传闻中的两次未来发布，存在一种推测而非证据的可能：其中 …
10月9日
10月8日
9月30日
- Leonardo de Moura Lean的战略优势，在于一个治理严格的核心，外围则是无需许可的扩展层。 Leonardo de Moura反对随机堆积 pull request，因为漏洞、未完成的功能和过早的设计承诺，可能束缚整个系统。Lean FRO如今由20人共同负责维护，将这项守护责任分散开来；而可扩展性则让外部开发者无需触碰可信核心，就能构建出令人意外的领域专用工具。
- 一次看似推翻Collatz猜想的证明，暴露了AI正在改变攻击证明检查器的经济学。 据称，这份提交同时利用了Lean官方内核中的1个漏洞，以及Rust实现的Nanoda检查器中的另一个无关漏洞；de Moura表示，他们确信这是AI生成的。Joachim的调查提出，某个LLM可能看过另一个代码仓库中的 pull request，随后拼出了这套攻击。结论在操作层面 …
- Kim Morrison借助AI开发的zlib项目，让形式化验证的底层软件从近乎不可行变得开始可行。 Claude Code代理将C代码翻译成Lean，实现了与C测试套件的兼容，证明对任意压缩级别和输入，压缩后再解压都能得到原始数据，随后又将大量使用数组的实现优化到接近Rust的方案。Scarfe说：“我们没有耐心做这种底层实现，但AI有。”
- Mathlib正面临AI放大的规模扩张问题，而不是定理产出不足。 Lean 4的库已经达到240万行，Lean 3则为110万行；de Moura引用的估计认为，要覆盖任意科学论文，代码规模可能需要达到1亿行。尽管Mathlib从2025年至今增长了44%，编译时间却下降了10%，AI仍可能让库的增长速度超过人类在性能优化和治理上的处理能力。
- 当前模型擅长有边界的“狙击式证明”，但在抽象、实验和选择正确方向上仍不可靠。 它们可以填补证明缺口、解释晦涩的内部机制，并在微观代码优化上胜过大多数人类，却仍会犯“愚蠢的错误”，而且往往是在复现既有技巧，而不是发明新方法。人类持久的角色在于品味：确定方向、组织库、选择值得解决的问题，并保留具备解释力的证明。
- 即便模型原始准确率接近99.99999%，机器可验证的证书仍不可或缺。 Boris Alekseev围绕单位距离猜想写下的120万行Lean证明，说明了为什么“没人想逐行检查这样的证明”。无论证明来自GPT-5.6、Claude Fable、蒙特卡洛树搜索还是未来的系统，Lean的机会都在于检查每一步，并逐步验证内核、编译器以及外围的信任链。