访谈/播客

Michael Freedman 的 π 日寄语：人工智能、数学发现与思维的未来

Happy π Day from Michael Freedman: AI, Mathematical Discovery, and the Future of Thought

访谈/播客🎤 主讲嘉宾 Michael Freedman（菲尔兹奖得主、Harvard 数学家、Logical Intelligence 首席数学家）；主持人 Chuck（SAIR 主持人）⏱ 18:33👁 NA

▶ 在 YouTube 观看

菲尔兹奖得主 Michael Freedman 在 π 日访谈中，结合自身经历探讨 AI 如何改变数学研究方式、人机协作的新角色，以及对原创性思维和数学本质的思考。

核心要点

与 AI 协作让数学家从「作者」变成「编辑」：AI 负责灵感与提出引理，人类负责逐行核查正误，恰是手摇计算器时代的反转。
当前模型在组合学、概率论、同调代数、代数几何等领域擅长提出引理，但在拓扑学与分析学中较弱，部分源于库的发展不均，也可能是学科基础概念契合度的内在差异。
AI 的突破来自放弃规则式编程、转向模仿大脑的神经网络；未来需要更大的上下文窗口、能量基模型（energy-based models）以及与 Lean 等形式化系统的对接来认证结果。
互联网已使科学发现民主化，AI 将进一步推动开放、协作式发现，未来约 3 年将处于人机协作模式。
AI 时代最重要的能力是原创性与「与众不同」，要警惕语法纠错、统一表达带来的思维同质化，保持思想多样性与独特视角。
新机遇在于「以统计方式整体地审视数学」——研究数学思维的本质、数学是发明还是发现，Freedman 团队提出「compression is all you need」作为数学本质的论点。

分章详解

π 日传统与走上数学之路

Freedman 与妻子都是跑步爱好者，属于少数想增重而非减重的人，冰箱里常备派；当天下午 3:14 他切了「一弧度（radians）」的南瓜派庆祝 π 日。
作为拓扑学家，他笑称自己很少用到 3.14159，但 π 在物理学里无处不在、出现在每个积分中，可能是他最喜欢的数学常数。
他走上数学之路，部分原因是「别的都不擅长、记性也不好」，只有数学这种自洽、系统化的学科能让他取得进展。
他提出一个观点：「你学的数学越多，需要记的反而越少。」并强调在信息丰富的时代，年轻人的教育重点应是判别、推理与思考，而非记忆。

AI 如何融入数学工作流：从作者到编辑

与 AI 协作就像批改作业或考卷：能拿到很多有趣的东西，但有些是错的，迫使人扮演「编辑」而非「作者」，要不断给 AI 的作业打分。
目前他用 AI 帮自己在不熟悉的领域证明引理（lemma），所谓引理指两到四页长度的命题。
AI 在组合学、概率论、同调代数、代数几何中较强，在拓扑学与分析学中较弱；他认为这既因库（libraries）发展不均，也可能是学科内在差异——代数中定理精确、可反复套用，而泛函分析、几何分析的论文常长达百页，因为很少能直接引用某条引理，必须按精神重新推导。
他形象描述：这与手摇计算器恰好相反——过去机器做枯燥细节、灵感来自人；如今 AI 提供灵感（虽多非真正全新，但因它读得多而对人来说像新点子），人类则负责逐行核查的「苦力活」。

AI 的技术演进与扩展挑战

AI 的重大进步来自放弃规则式编程：1980 年代 IBM 的 Deep Blue／Deep Thought 是规则式国际象棋的极限，而 AlphaGo、Alpha Chess 表明用神经网络模仿人脑结构更有效；未来可能走向能量基模型（energy-based models）。
AI 智能体需被赋予「宪法式」的约束限制，以服务人类需求、不致脱轨，但其大部分思考将不是规则式的。
当前语言模型是自回归（autoregressive）的，一旦跑偏就难以拉回；若要让智能体不只证明引理、而是开展整个研究项目，就需要更大的上下文窗口，自回归模型可能不够，需要能量基模型等新方向。
他强调必须与 Lean 等形式化系统直接对接，使已取得的进展能被认证、验证并随研究推进存入数据库；并称赞 Lean 创始人 Leo de Moura。

发现的民主化与协作模式

Freedman 认为我们已进入开放协作的时代：互联网极大地民主化了科学发现，过去必须身处 Princeton、Harvard 等名校才能接触前沿，如今数百所州立大学也能做出同样出色的工作。
技术工具使大规模协作成为可能，人机协作模式正快速演进，他预计未来约 3 年将以这种协作模式为主，人类扮演 AI 的编辑角色。
这一 π 日倡议的愿景之一，是让 AI 使更多人能有意义地参与数学与科学发现，形成自下而上的草根力量。

下一代人才：原创性与思想多样性

他认为最重要的，是「你所知与众人所知之间的对称差」——即个人的独特性（idiosyncrasy）比以往任何时候都重要。
互联网与语法纠错工具正使个人视角流失，把每个人推向相同的写作与思维风格；但「离群」未必是错误，人们本就有不同的思考与表达方式。
他以耶鲁学派的 Rommel 等「看世界方式不同」的人为例，警示表达、记号、观点同质化的风险，强调要保持思想多样性与「奇怪」的视角。
他主张人们仍应学习编程以理解幕后原理，并学习经典、人文与历史；建议年轻人保持原创和一点「古怪」，比如那些把头发染成怪颜色的孩子的那种思维。

AGI、历史加速与数学的本质

关于 AGI 能否近期实现，他认为「两者皆是」：即使没有新突破，仅对过去十年成果的精炼就会带来巨大进步；同时数万名聪明人投入，也必会带来全新突破。
他描述文明约 1.1 万年历史（自农业起步），近 600 年经文艺复兴、启蒙、科学革命、工业革命到信息时代呈指数式加速，呼应 Fukuyama 所谓「历史的终结」；如今「遥远的未来」已从百年缩短到约 4 年。
他用近乎宗教的比喻：人类长期在「建造神明」，但这是第一次要为之支付电费——闪电曾是免费的，如今我们造出了一个了解我们一切的新「智识种族」，赤裸地站在它面前。
他指出新机遇是「审视数学而非只做数学」：以统计方式整体地研究数学这一过去个人无法做到的事，追问数学思维的本质、数学是发明还是发现；并预告所在公司 Logical Intelligence 全组将发表论文《Compression is all you need》，提出数学的本质在于某种信息压缩。
他补充：即便电子智能体比人快百万倍，相对于任意演绎的双重指数爆炸仍是小因子，绝大多数演绎（如 NP 完全问题的实例）都枯燥无趣，人类及其智能体只会探索所有可能逻辑演绎中极薄的一条「丝带」。

关键引述

“「与 AI 协作，把我们置于编辑而非作者的位置——我们得不断地给它们的作业打分。」（it sort of puts us in the position of an editor rather than an author when we collaborate with AIs. We have to constantly be grading their homework）”— Michael Freedman

“「它的职责是提供灵感，而你被留下做逐行检查、看它哪里搞砸了的苦力活。所以这有点像手摇计算器的反面。」（its responsibility is the inspiration, and then you're left with the grunt work of going through line by line... it's kind of like the opposite of a hand calculator）”— Michael Freedman

“「数学学得越多，需要记的反而越少。」（the more mathematics you study, the less you have to know）”— Michael Freedman

“「人类长期从事建造神明的事业，但这是第一次我们得为它付电费——闪电曾经免费，现在我们得为它买单并与之共处。」（humanity has been in the business... of constructing deities, but this is the first time we're stuck with the electric bill）”— Michael Freedman

“「做到原创、并且有点古怪，将变得非常重要。」（being original and a little bit strange it will be very important）”— Michael Freedman

术语 / 人物

Michael Freedman — 美国数学家，1986 年因证明四维庞加莱猜想获菲尔兹奖；曾任 Microsoft Research 量子计算项目创始主任，现任 Harvard CMSA 半职研究员及 AI 公司 Logical Intelligence 首席数学家。

四维庞加莱猜想（four-dimensional Poincaré conjecture） — 拓扑学中对四维空间结构进行分类的里程碑式定理，Freedman 的证明使他获得菲尔兹奖。

引理（lemma） — 用于证明更大定理的中间命题；Freedman 指他用 AI 帮助证明约两到四页长度的引理。

能量基模型（energy-based models, EBM） — 为候选状态或推理过程打一个标量「能量」分的模型，能量越低表示越符合约束与目标；被视为超越自回归语言模型、推进数学推理的方向。

自回归模型（autoregressive model） — 逐词预测生成的语言模型范式，优点显著但一旦推理跑偏便难以拉回正轨。

Lean — 由 Leo de Moura 创立的形式化证明助手与编程语言，可对数学证明进行机器认证与验证。

Logical Intelligence — Freedman 参与的 AI 研究公司，将 Lean 式形式化推理与大语言模型、能量基模型结合；预告论文《Compression is all you need》探讨数学本质即信息压缩。

元数学（meta-mathematics） — 用数学方法研究数学本身的领域，涉及哲学与逻辑，因逻辑可嵌入数学而具自指性。

背景补充

Michael Freedman（生于 1951 年）是美国数学家，1986 年因证明四维庞加莱猜想获菲尔兹奖，并获国家科学奖章、Veblen 奖与 MacArthur 学者称号，是美国国家科学院院士。1998 年他成为首位离开学术界进入工业界的菲尔兹奖得主，加入 Microsoft Research 并创立其量子计算项目。如今他在 Harvard 数学科学与应用中心（CMSA）任半职研究员，并担任 AI 初创公司 Logical Intelligence 的首席数学家；该公司汇集顶尖数学人才，专注于将 Lean 式形式化推理与能量基模型相结合。本视频为 SAIR（科学与 AI 研究基金会，由陶哲轩等联合创立）的 π 日访谈系列之一。

适合谁看

适合关心 AI 与数学／科学交叉、人机协作研究范式、形式化验证（Lean）与 AGI 前景的研究者、学生与科技从业者，以及对数学本质与思维未来感兴趣的广泛读者。