竞赛/平台指南

陶哲轩(Terence Tao)：SAIR 的数学竞赛

Terence Tao: Mathematics competitions at SAIR

竞赛/平台指南🎤 陶哲轩 (Terence Tao)⏱ 11:15👁 NA

▶ 在 YouTube 观看

陶哲轩远程介绍 SAIR 正在举办的数学竞赛——以「蒸馏挑战」和「模算术挑战」为代表，旨在为 AI 时代的数学建立新的「交通基础设施」，让开源模型逼近前沿模型水平。

核心要点

AI 已让数学的传统发表渠道（期刊、论坛、众包项目）陷入「AI 生成内容大堵车」，许多平台被迫限制甚至封禁 AI。
陶哲轩主张为人类与 AI 分设不同「车道」，建立新基础设施，而 SAIR 竞赛正是这一思路的实践。
首个竞赛是「蒸馏挑战」：把 2200 万个泛代数真假问题的知识压缩成一页「小抄」，让廉价开源模型达到前沿模型水平。
第一阶段（真假判断）已结束，「小抄」让开源模型表现提升约 20–30%，且在难题上的提升差异更值得研究。
第二阶段要求模型用 Lean 形式语言给出证明，并设「单题模式」与「马拉松模式」考验资源分配能力。
即将推出「模算术挑战」，比拼设计极小的 transformer 高速完成模运算，未来还计划拓展到物理、化学等领域。

分章详解

开场与背景：AI 给数学带来的「巨变」

陶哲轩因另有会议安排无法到场，改以录制视频汇报 SAIR 正在开展的数学竞赛活动。
他指出当前有一个竞赛进行中、另一个预计当天（视频录制时）发布。
AI 正对数学的传统工作流造成「巨变」(sea change)：期刊、在线论坛、众包项目都在经历 AI 生成内容的「交通堵塞」。
AI 模型已能生成大量证明，相当一部分是正确的、甚至可被形式化工具自动验证，但写作质量差、人类不愿审阅，净价值很低。

传统渠道的饱和：以 Erdős 问题网站为例

面对 AI 洪流，许多传统数学渠道大幅限制乃至直接封禁 AI 的使用。
以 Erdős 问题网站为例：过去通常同时只有一两个待审解答，社区尚可合理审阅。
自 GPT-5.5 发布后，单个问题涌入数十个待定解答，远超人类核验能力。
当某问题挂着一个未确认的 AI 证明时，人类反而失去研究动力——因为不知道它到底解没解，处于「灰色地带」。

解决思路：为人类和 AI 分设「车道」

陶哲轩用「汽车发明初期道路仍按 19 世纪马车设计、缺乏交通法规」作类比，形容当下的混乱与拥堵。
应对之道是建立新的基础设施，而非把人类数学与 AI 数学硬塞进同一车道。
为人类、为 AI、尤其为高速自动化 AI 分设不同车道，才能兼得高效高质的定理生产与人类可消化的精华成果。
SAIR 竞赛正是为提供这种新基础设施而设计。

首个竞赛：蒸馏挑战（Distillation Challenge）

竞赛于 Pi Day（3 月 14 日）启动，建立在陶哲轩约两年前的众包项目之上。
该前置项目动用约 50 人和大量 AI（非顶尖大模型，而是更老的自动定理证明器），解决了一组 2200 万个泛代数真假问题。
举例：若代数关系星号满足 x·y·z = z·w·w，是否也满足 x·y·z = x·y·z——多数题研究生半小时可解，但总量高达 2200 万。
用前沿模型（如 Gemini Deep Think）逐题求解虽可给出正确反证，但跑完 2200 万题需数周、耗资数十万美元；开源模型则仅略好于 50% 随机水平。
挑战目标：把全部已知解答的知识「蒸馏」成一页「小抄」(cheat sheet)，让开源模型达到前沿模型水平，同时让人类读懂该领域最核心的事实。

竞赛机制与第一阶段成果

选手提交一页提示词（prompt），在多个模型上测试；理想的「小抄」不应过拟合单一模型，要让任何「中等生」都能提分，并兼具人类与大模型的可读性。
第一阶段只判断真假，要求成功率高于 50%；第二阶段升级为用 Lean 形式语言给出证明，并允许访问 Python 代码。
第二阶段设两类挑战：「单题模式」逐题尽力求解；「马拉松模式」一次给 100 题但算力有限，须像考长卷的学生一样分配 token 优先级。
强调开源共享：选手须把模型提交到定制的贡献者网络，供他人引用与改进，已有数百份「小抄」相互迭代、社区氛围友好。
第一阶段成果：小抄让开源模型在随机题上的表现提升约 20–30%；在超难题上提升差异更大（部分模型更明显），原因尚待解释。
竞赛设有排行榜（leaderboard），选手可按不同指标展示成绩；竞赛仍在进行中。

下一个竞赛与未来展望

即将推出「模算术挑战」(modular arithmetic challenge)：模算术即「时钟算术」，在密码学等场景中应用极广。
目标是设计极轻量、廉价的电路/极小 transformer，尽可能快地完成 5、10、20 位的模运算；此类任务过去多由人工设计，现可借机器学习创新。
该挑战易于基准测试，期待选手用最新 AI 工具找出有创意的解法。
SAIR 正筹备更多竞赛，并计划拓展到物理、化学等领域，认为 AI 辅助的高速竞赛具有真实的科学价值。

关键引述

“所有数学家投稿的常规渠道——期刊、在线论坛、众包项目——都越来越多地遭遇 AI 生成内容造成的「交通堵塞」。”— 陶哲轩 (Terence Tao)

“这种情形就像汽车被发明出来，但道路和街道仍是为 19 世纪的交通——行人、马匹和马车——而建，而且我们还没有制定交通法规。”— 陶哲轩 (Terence Tao)

“与其把人类生成的数学和 AI 生成的数学硬塞进同一条车道，不如给人类一些车道、给 AI 一些车道，尤其给自动化高速 AI 专门的车道。”— 陶哲轩 (Terence Tao)

“我们能否把 2200 万个代数解答的知识，浓缩进一张一页的「小抄」里，交给开源模型，让它达到前沿模型的水平？”— 陶哲轩 (Terence Tao)

“我认为这里有很大空间去开展 AI 辅助的、高速的、真正具有科学价值的竞赛。”— 陶哲轩 (Terence Tao)

术语 / 人物

SAIR（科学与 AI 研究基金会，Foundation for Science and AI Research） — 由陶哲轩等联合创立的机构，汇聚诺贝尔奖、图灵奖、菲尔兹奖得主，旨在用 AI 加速科学发现、并以科学夯实 AI 的基础，开放数据、基准、工具与模型并举办 SAIR 竞赛。

蒸馏挑战（Distillation Challenge） — SAIR 首个竞赛，要求把 2200 万泛代数真假问题的知识压缩成一页人类可读的「小抄」，帮助开源大模型逼近前沿模型的解题水平。

泛代数 / 方程理论项目（Equational Theory Project, ETP） — 陶哲轩约两年前发起的众包项目，约 50 人配合自动定理证明器，解决了一组 2200 万个关于代数恒等式的真假问题。

Lean — 一种形式化证明语言，竞赛第二阶段要求模型用它给出可机器验证的证明。

模算术（modular arithmetic，「时钟算术」） — 对整数取模后的算术运算，在密码学中应用广泛；SAIR 下一个挑战要求设计极小 transformer 高速完成此类运算。

自动定理证明器（Automated Theorem Provers） — 早于大语言模型的一类 AI 工具，ETP 项目用其批量求解大量代数问题。

背景补充

陶哲轩 (Terence Tao) 是加州大学洛杉矶分校教授、菲尔兹奖得主，被誉为当代最杰出的数学家之一，长期推动「Polymath」式的大规模开放协作与 AI 辅助数学。SAIR（科学与 AI 研究基金会）由他与多位诺贝尔奖、图灵奖、菲尔兹奖得主联合创立，致力于用 AI 加速科学发现并以科学夯实 AI。其首个竞赛「数学蒸馏挑战——方程理论」由 Damek Davis 与陶哲轩发起，于 2026 年 3 月 14 日（Pi Day）启动，基于方程理论项目的 2200 万个已解问题，托管于 competition.sair.foundation。

适合谁看

适合关注 AI 与数学交叉、形式化证明、开源大模型评测的研究者与工程师，以及对竞赛式科研协作与「人机分流」新型科研基础设施感兴趣的读者。