205
1节目简介：
本期来自SAIR在加州理工学院举办的 Science x AI Summit。菲尔兹奖得主、SAIR Foundation联合创始人陶哲轩发表主题演讲，预告SAIR的Open Math Model initiative；2026年9月18日，SAIR正式启动「开放数学模型计划」。
陶哲轩将数学问题求解分解为三个环节：证明生成、证明验证、证明消化。他指出，前两个环节正被AI以远超第三者的速度自动化，由此产生了 proof indigestion——证明被生成、甚至被验证，却没有被消化。“消化”的定义是：理解证明为何成立、连接已有文献、提取可迁移的思想。
同日，陶哲轩与24位菲尔兹奖得主联合发布声明《A Severe Misalignment of AI in Mathematics》，指出AI公司将“解决著名未解问题”作为能力基准的做法，可能与数学共同体追求理解、洞察与人才培养的核心目标产生错位。
SAIR的回应：与数学社区共同构建开放权重模型与开源工具，首阶段聚焦理解论证、核对文献、形式化证明，坚持开放权重、可复现评测与社区治理。演讲也介绍了Distillation、Inverse Galois、Andrews-Curtis、Lean Kernel四项竞赛。
Shownotes：
嘉宾：陶哲轩（Terence Tao），菲尔兹奖得主、SAIR Foundation联合创始人
场合：Science x AI Summit at Caltech，2026年9月11日
主办：SAIR、Caltech、Merkin Center for Pure and Applied Mathematics
正式启动：2026年9月18日，SAIR「开放数学模型计划」
时间轴：
00:00 数学的价值：不止于求解问题
04:54 AI生成与验证证明的速度与理解瓶颈
07:34 SAIR开放数学模型计划
10:37 将代数知识蒸馏为提示与程序
13:59 逆伽罗瓦挑战：从竞赛到协作
17:54 对齐AI激励与数学价值
21:21 保存人类洞察与数学知识质量
标签：
#SAIR #陶哲轩 #AIforMath #开放科学 #数学 #形式化证明
