Lobsters | 📄 原文链接 | 2026-10-14 收录

Vi Hart 谈 OpenAI 的纳维-斯托克斯「证明」

来源：patreon.com — 2026-10-11

📋 概述

Vi Hart 用六节长文拆解 OpenAI 宣称以 Lean 验证了纳维-斯托克斯问题的消息。她自曝曾短暂在微软研究院参与 Lean 项目做项目管理，因此清楚这类能力「不是靠偶然或自然演化发展出来的，而是需要意图、项目规划和大量时间与金钱」。她认为 OpenAI 的结果之所以可能，靠的是五年来庞大的大学数学家、学生与业余志愿者把数学形式化进 Mathlib，以及无数程序员和从业者的无偿产出；而她当年的五年计划里就设想过千禧年难题被 Lean 验证的那一天，所以并不为「88 小时」惊讶。她还用「巴别图书馆式的 Mathlib」反驳 AI 能凭空生成数学：脱离人类语境，把所有证明罗列出来与按序罗列整数一样没有意义，LLM 只是去人已经写过的地方才不会翻车。

🔑 核心要点

作者身份：曾在微软研究院短暂参与 Lean 项目做项目管理，清楚这项技术是怎么积累出来的
技术不会自己长出来：它需要意图、项目规划，以及如此多的时间与金钱
结果的真正底座是五年多来大学数学家、学生与业余志愿者把数学形式化进 Mathlib，加上无数无偿的开源代码与问答
她说自己在 2021 年的五年计划里就设想过千禧年难题被 Lean 验证，因此对 2026 年的宣布毫无惊讶
「Mathlib 巴别图书馆」论证：脱离人类语境，罗列所有证明与按序罗列整数一样没有意义
她的经验判据：凡是看起来很棒的 AI 产出，一定意味着该领域已有大量人类数据，AI 不可能自己跳到那里

💡 金句

这种技术不是靠偶然或自然演化发展出来的，它需要意图、项目规划，以及如此多的时间与金钱。

← 返回 Lobsters 首页