在这场名为《Carina Hong: Frontiers of AI for Mathematical Research》的演讲中，Axiom 的创始人兼 CEO Carina Hong 详细分享了 AI 在数学研究领域的最新前沿进展、所面临的挑战以及他们团队取得的突破性成果。
以下是演讲内容的详细梳理：
一、 Axiom 的愿景与技术路线
- 团队与目标： Axiom 是一个位于帕罗奥图（Palo Alto）的 40-45 人团队，专注于推进形式化数学（Formal Mathematics）以及可验证推理（Verified Reasoning）的前沿 [00:00]。
- 核心理念： 团队相信，如果在数学推理任务上取得重大进展，其成果将 100% 形式化并基于 Lean 语言 进行验证，这可以无缝迁移到软件和硬件验证等对安全性要求极高的重要领域 [00:13]。
- 技术架构： Axiom 采用混合系统（Hybrid System） [02:29]。他们基于开源大语言模型进行微调，使其能够生成 Lean 验证的证明，并结合多模型智能体系统（Agent System）、传统自动定理证明（ATP）技术、测试时计算量扩展（Inference Scaling）、递归分解以及回溯等技术，使系统性能远超单一模型 [09:14, 14:04]。
二、 AI 在数学竞赛上的演进历程
Carina 梳理了过去两年（2024-2025年）AI 在数学竞赛上的惊人突破：
- 早期（AlphaProof 时代）： 主要将数学问题转化为 Lean 语言，在结构化数据域内利用训练时的蒙特卡洛树搜索（MCTS）进行强化学习 [01:05]。
- 2025年7月 IMO（国际数学奥林匹克）： 迎来了非形式化（Informal）模型的爆发。OpenAI（如 01 系列模型）和 Google DeepMind（Gemini）通过思维链（Chain of Thought）和测试时扩展（Scaling Test Time），完全用自然语言推理拿到了 IMO 金牌。同时，Harmonic 和字节跳动的形式化数学实验室也取得了顶尖成果 [01:26]。
- 2025年12月 Putnam（普特南数学竞赛）： 面对广泛的大学本科级数学题，Axiom 团队斩获了完美满分（Perfect Score）。在实时竞赛的有限时间内，AI 先解出了 12 道题中的 8 道，并最终在 12 月完成了全部题目的 Lean 证明 [02:11]。
三、 从数学竞赛走向“数学研究”的痛点
尽管竞赛成绩惊人，但 Carina 强调，竞赛数学与真正的数学研究有着巨大的鸿沟。目前阻碍 AI 数学研究发展的最大问题在于缺乏公认的、统一的基准测试（Benchmarks） [03:44]：
- 寻找未解之谜困难： 未解的科研问题往往是教授和研究生的“知识产权”，很难像机器学习那样组装出包含 500 道题的规模化标准集 [04:03]。
- 现有基准的局限性：
- FrontierMath (Tier 4)： 虽然题目极难，但它专为非形式化推理设计，为了方便自动评判，所有问题都被迫压缩成“只有一个数字答案”，而绝大多数数学研究需要的是复杂的证明 [04:20]。
- DeepMind 的形式化猜想集： 难度分布过于两极分化，既有相对简单的厄多斯（Erdős）问题，也有价值百万美元的“千禧年大奖难题”，导致无法科学地衡量 AI 系统的均等进步 [04:53]。
- First Proof： 包含 10 个博士级的难题。目前的尖端大模型和初创公司基本都折戟于此。更有趣的是，由于目前 Lean 库的覆盖范围有限，这些问题在 Lean 中甚至无法被形式化陈述 [05:27]。
四、 厄多斯（Erdős）难题的“宝可梦捕捉”热潮
由于缺乏统一的 Benchmark，目前各大 AI 实验室演变成了针对具体数学难题的“狩猎赛”：
- 技术乌龙与反转： 2025年10月，OpenAI 声称 GPT-5 解决了 10 个未解的 Erdős 问题，但随后被 DeepMind “打脸”指出这只是文献检索（AI 只是搜到了前人的成果）。Axiom 和 Harmonic 早期也曾误以为自己独立解出了某些问题 [06:19]。
- 最新进展： 2026年，社区决定像当年“预测蛋白质结构”一样，对 Erdős 课题库发起全面总攻。目前在专门的 GitHub 仓库中，至少有十几道此前未解的 Erdős 问题被 AI 独立攻克 [06:57]。不过 Carina 也指出，Erdős 组合数学问题的风格依然偏向竞赛数学，AI 需要走得更深 [07:44]。
五、 Axiom 的硬核科研成果：100天 7 篇论文
Carina 自豪地展示了 Axiom 自 2026 年 2 月初以来，在100天内向公众推出的 7 篇数学研究论文（其中 3 篇已被正式数学期刊接收） [08:03]。这其中包括 5 篇形式化定理证明和 2 篇自动形式化（Auto-formalization）论文。
她详细介绍了两个极具代表性的数论突破：
- 几乎所有素数都是部分正则的（Almost all primes are partially regular）： 针对 1929 年提出的关于代数数论中理想类群“偶数部分空间（Even Subspaces）”是否会消亡的经典猜想，Axiom Prover 证明了：对于几乎所有的素数 $p$，其偶数部分空间的很大一部分都会消亡。这是关于该偶数空间的首个无限理论成果，论文已被《Archiv der Mathematik》接收 [09:50]。
- 拉马努金 $\tau$ 函数的非素数性（Ramanujan $\tau$ Function）： 研究拉马努金 $\tau$ 函数（模判别式的傅里叶系数）何时会取素数值。这是一个巨大的谜团（例如直到 $251^2$ 时才会出现一个庞大的素数值）。在假设 ABC 猜想成立的前提下，Axiom Prover 证明了：该函数避开了 100% 的素数（即其取值为素数的集合密度为零）。该论文已被《Indagationes Mathematicae》接收 [11:20]。
💡 复杂度的飞跃： 从 2025 年 12 月解决 Erdős 124 问题到 2026 年 3 月解决拉马努金 $\tau$ 函数问题，AI 生成的证明图谱（Proof Graph）复杂度从 不足 50 个推理节点飙升到了约 500 个推理节点 [12:45]。
六、 自动形式化与人类协同
除了独立证明，AI 还能帮助形式化人类数学家的已有成果（将自然语言证明翻译为 Lean 代码，其推理图谱的复杂度不亚于独立定理证明） [08:36]：
- 成功自动形式化了一篇关于正点阵三角形（处理台球与动力系统）的复杂论文 [13:30]。
- 成功自动形式化了 Eon Huang 关于有理节点威特（rational node Witt）的二次型推广论文，展现了新型的“人机协作”模式 [13:36]。
七、 未来路线图与社区贡献
Carina 总结道，“AI for Mathematics”的时代已经真正到来。
Top comments (0)