主题演讲

Carina Hong：AI 用于数学研究的前沿

Carina Hong: Frontiers of AI for Mathematical Research

主题演讲🎤 Carina Hong（洪乐彤，Axiom 创始人兼 CEO）⏱ 15:02👁 NA

▶ 在 YouTube 观看

Axiom 创始人 Carina Hong 阐述 AI 数学已从奥数竞赛迈向真正的数学研究，并展示其「形式化+非形式化」混合系统在数论等领域的研究级成果与基准测试困境。

核心要点

AI 数学的焦点正从受限的数学奥林匹克（IMO、Putnam）转向开放的数学研究问题，后者是「AI for Science」的理论底层。
研究级数学缺乏公认的评测基准：问题稀缺、属于教授的知识产权、且大多需要证明而非单一数值答案，使得难以做到机器学习式的大规模 benchmark。
在基准缺位下，业界出现「分享单点胜利」的趋势，Hong 称之为「数学版宝可梦狩猎」，并指出 OpenAI 等所谓「解决 Erdős 问题」常被发现只是文献检索。
Axiom 采用混合系统：在开源 LLM 基础上训练可产出 Lean 可验证证明的模型，并用多模型 agent 框架与工具调用把性能推到超越任何单一模型。
Axiom 100 天内在 arXiv 发表 7 篇数学论文，3 篇被期刊接收，涵盖数论、交换代数、代数几何及自动形式化（autoformalization）。
代表性成果包括「几乎所有素数都是部分正则的」（被 Archive de Mathématique 接收）和关于 Ramanujan tau 函数取素数值密度为零的结果（被 Indagationes Mathematicae 接收）。

分章详解

公司与愿景：用形式化数学推动可验证推理

Axiom 位于 Palo Alto，约 40-45 人，致力于推动形式化数学与「可验证推理（verified reasoning）」的前沿。
核心信念：若 AI 在数学推理上取得真正进展，可迁移到其他重要领域；尤其当数学是 100% 经验证并扎根于 Lean（形式化验证语言）时。
由此可延伸到软件与硬件验证等应用领域。

从奥数到研究：AI 数学的近期里程碑

2024 年 7 月 DeepMind 的 AlphaProof 在 IMO 拿到 28/42（银牌，仅差一分摘金），靠的是把数学转成 Lean 并用蒙特卡洛树搜索等结构化方法，类似下棋。
2025 年 7 月转向「非形式化」模型：OpenAI 与 Google DeepMind Gemini 完全用自然语言推理（承接 2024 年 9 月 o1 推理模型革命、思维链、测试时扩展）拿到 IMO 金牌；Harmonic 与 ByteDance 则走形式化路线也取得超越赛时的优异表现。
12 月 Putnam（本科级、考纲广）中，Axiom 实时参赛得 8/12，12 月最终解出全部 12 题报告满分，并公开全部证明；其输出为 Lean，但系统内部也有非形式化模型参与（混合系统）。

为何要做研究数学：AI for Science 的理论底层

物理、化学、神经科学等大量应用问题缺乏数学理解，但很少有数学家愿意深入到完全不同的领域去帮助应用科学家。
举例：中国剩余定理（初等数论的基础结果）被 MIT 的 Elowitz 实验室用于计算神经容量；某些量子能级间距可用素数间距建模。
若能造出会做研究（而非仅做受限奥数题）的 AI 数学家，不同领域的思想或可相互融合，这或许是 AI for math 的「圣杯」。

评测难题：研究数学缺乏公认基准

奥数 benchmark 易做（有历年试题、训练营、教练标注），但研究数学难：未解问题属于教授的知识产权，难以攒到机器学习意义上至少 500 题的规模。
FrontierMath Tier 4（OpenAI 与 Epoch AI 合作的私有基准）面向非形式化推理、所有问题只有一个数值答案，但研究数学大多需要证明，评分很难。
Google DeepMind 的形式化猜想基准难度跨度过大，从 Erdős 问题到千禧年大奖难题，分布不均匀；FrontierProof（约 30 位著名数学家、10 道博士级题）框定保守却让众多前沿大模型与创业公司失败，且多数题目至今无法在 Lean 中形式化。

Erdős 问题热潮与「宝可梦狩猎」现象

Erdős 问题来自 Hong 的朋友兼同行 Thomas Bloom 维护的仓库，今年成为 AI for math 的焦点。
去年 10 月 OpenAI 称 GPT-5 找到 10 个此前未解 Erdős 问题的解，但被竞争对手 DeepMind 指出「found」实为文献检索；Harmonic 与 Axiom 也曾在 Erdős 124、481 上声称匹配，结果文献中早有解。
随后业界像「折叠 2 亿蛋白质」一样逐题尝试每个 Erdős 问题，已有至少十几个此前未解问题被独立解决；在基准缺位下，「分享单点胜利」成为趋势，Hong 称之为「数学版宝可梦狩猎」；也有人主张应跳出组合数学，因为 Erdős 问题在风格与深度上与奥数题相近。

Axiom 的研究成果与代表性定理

自 2 月初首篇关于 Faltings 猜想（数论）的研究论文起，100 天内推出 7 篇 arXiv 论文，3 篇被 Archive de Mathématique、Indagationes Mathematicae、Research in Mathematical Sciences 接收；其中 5 篇为形式化定理证明，2 篇为自动形式化。
成果一：「几乎所有素数都是部分正则的」——Kummer 判据的 Galois 精化中，奇子空间由 Herbrand-Ribet 定理（与费马大定理相关）较好理解，而偶子空间自 1929 年起被猜测全部消失但未获证；Axiom Provers 证明了对几乎所有素数 P，偶子空间的很大一部分确实消失，这是已知关于偶子空间的第一个无穷定理（被 Archive de Mathématique 接收）。
成果二：Ramanujan tau 函数（模判别式 delta 的系数，是否取零即著名 Lehmer 猜想）何时取素数值——首个较大素数出现在 251 的平方附近；在 ABC 猜想假设下，Axiom Prover 证明 tau 错过 100% 的素数（即取素数值的集合虽无穷但密度为零，被 Indagationes Mathematicae 接收）。
推理规模从 Erdős 124（约 50 个推理节点）增长到 Ramanujan tau（约 500 个推理节点）。

方法、人机协作与未来方向

Axiom 是混合方法：在开源 LLM 上训练可产出 Lean 验证证明的模型，再把多个模型组合进一个 agent 框架并配以优秀工具调用，结合现代后训练代码生成与传统自动定理证明技术。
自动形式化（把已有非形式化证明转成 Lean）技术难度不亚于形式化定理证明，需产生同等复杂的推理图；案例包括关于正格三角形/台球与动力系统的论文，以及 Efron Huang 关于二次型推广的论文。
经验教训：AI for math 已经到来，建议大家用现有 AI 与形式化验证工具尝试；专家知识、选对问题、扩展推理时计算、递归分解与回溯都很有帮助；Lean 基础设施很重要，为此免费发布了工具 Axo（含十余种工具便利证明验证与代码操作）。
未来方向：处于猜想生成、库学习（提出有趣定义）研究的起点；应把 AI 数学发现文献（如 Explorer、AxSolver，pattern booster 的扩展，以及开源的 Axiom 产品）整合进同一工作流，让例子、反例、构造与证明协同。

关键引述

“在基准缺位时，分享具体问题上的胜利成了一种风潮——这有点像数学版的宝可梦狩猎：今天我找个目标，用我的技术试一试，赢了就告诉全世界，输了就没人知道。（When benchmark is absent, sharing wins on specific problems becomes a trend. It's a little bit like mathematical Pokémon hunting.）”— Carina Hong

“事实证明，所谓「found（找到）」指的是文献检索——这一点被它的竞争对手 Google DeepMind 揭穿了。（It turns out that found refers to literature search, as called out by Google DeepMind.）”— Carina Hong

“AI for math 已经到来。挑一个你最喜欢的结果，用手边的 AI 工具去试，也请试试形式化验证这一侧的工具。（AI for mathematics is here. Choose your favorite result, try it with the AI tools available to you, and please try the formal verification tools as well.）”— Carina Hong

“我们在最底层做的，其实是 AI for science 的理论层。（What we are doing at the bottom heart is a theoretical layer of AI for science.）”— Carina Hong

术语 / 人物

Axiom — Carina Hong 于 2025 年创立的 AI 数学创业公司，位于 Palo Alto，约 40-45 人，目标是构建会做研究的「AI 数学家」并产出 Lean 可验证证明。

Lean — 一种形式化验证的编程语言/证明助手，可对数学证明做机器级验证，是 Axiom 输出可验证证明的基础。

Autoformalization（自动形式化） — 把已有的非形式化（自然语言）数学证明自动转换为 Lean 版本的技术，难度不亚于形式化定理证明本身。

AlphaProof — DeepMind 的形式化定理证明系统，2024 年 7 月在 IMO 取得 28/42（银牌），用 Lean 与蒙特卡洛树搜索等结构化方法。

Putnam 竞赛 — 北美著名的本科生数学竞赛，考纲广；Axiom 报告其系统取得满分（实时赛时 8/12，12 月解出全部题目）。

Erdős 问题 — 由 Thomas Bloom 维护的 Paul Erdős 未解问题仓库，今年成为 AI for math 的焦点；与奥数题在风格深度上被认为相近。

Herbrand-Ribet 定理 — 代数数论结果，刻画分圆域类群奇子空间，与费马大定理密切相关；Axiom 的成果则处理此前未知的偶子空间。

Ramanujan tau 函数 — 模判别式 delta 的系数，数论中的核心对象；其是否取零即著名的 Lehmer 猜想，Axiom 证明它取素数值的密度为零（在 ABC 猜想下）。

Axo — Axiom 免费发布给社区的 Lean 工具集，含十余种工具，便利证明验证与代码操作以提升 Lean 基础设施速度。

背景补充

Carina（Letong）Hong 是 Axiom Math 的联合创始人兼 CEO，约 24 岁，MIT 数学与物理双学位、Rhodes 学者、Morgan Prize 得主，曾在 Stanford 攻读数学博士后退学创业。Axiom 主张「数学即代码、代码即数学」，用 Lean 的真值奖励信号训练模型以提升样本效率，并将形式化验证视为扩展超级智能的关键。公司发展迅速，曾报道获 B Capital 领投的 6400 万美元种子轮，后在其 AI 取得 Putnam 满分后以约 16 亿美元估值再融 2 亿美元，团队汇集来自 Meta FAIR、DeepMind 的研究者及数学家 Ken Ono。

适合谁看

适合关注 AI for math/形式化数学（Lean、自动定理证明）的研究者与工程师，以及想了解 AI 如何从奥数走向真正数学研究及其评测难题的科技从业者与投资人。