数理科学 · OECD FoS 1.1 · 教育部 0701 数学
数学
Mathematics
L3系统改造 ↑ 上升 ↓ 由 L4 降级 综合分 2.90 · 上次复审 2026-10-22 · 下次复审 2026-12-20
最大突破 2026-10-11 AI 飞跃学科飞跃
Banks 逐行核验并重写 OpenAI 的“朗道–西格尔零点不存在”证明，给出显式常数（q₀=10¹⁰，δ₀=3.0×10⁻³） ↗
AI：OpenAI 模型给出解析数论近百年核心难题的证明（2026-10-01 手稿），密苏里大学 Banks 逐行核验并称论证成立，Kerr 另给出更简证明（arXiv 2610.21099），Lean 形式化经两个独立内核复核；学科：西格尔零点阻碍算术级数素数分布与类数的有效估计，若最终确认将改写多个经典结果（尚未经期刊审稿，陶哲轩称仍在消化）
分级理由
数学是 AI 科学发现最强的学科：2026-05 OpenAI 模型推翻 1946 年 Erdős 单位距离猜想（Alon、Gowers、Sawin 等 9 位数学家写了人类核验版），PNAS 发表 AlphaEvolve 在 67 个问题上的系统探索，DeepMind 智能体在 Lean 中独立解决 9 个 Erdős 公开问题。但从业者普遍采用和课程改革尚未发生，openai/math 还出现撤回和公开抵制，所以综合定为 L3（发现维度 4 分）。
↓ L4 → L3
S = 0.30·method + 0.35·discovery + 0.25·adoption + 0.10·education（教育缺证据时记 0 分；若为空则按其余权重归一）
依据来源
综合分 2.5–3.49（或 ≥3.5 但方法/发现/采用有一项低于 3）：AI 成为标准基础设施或业务流程，多项独立突破。 全部分级标准 →
研究方向
形式化证明（Lean）自动形式化大模型推理求解开放问题进化式算法搜索（AlphaEvolve）竞赛数学
论文
- An orthogonality inequality in $\mathbb{RP}^{n-1}$ and the double-cap conjecture 人类数学家借助 AI 证明“双帽猜想”（球面上无正交点对的集合测度上限），主结论另有几乎完全由 AI 完成形式化的 Lean 4 证明
AI：作者在摘要中说明 AI 协助撰写论文，主不等式和双帽结论的另一份 Lean 4 证明几乎完全由 AI 工具完成形式化与验证；学科：双帽猜想是球面上“无正交对集合”测度的长期公开问题，论文同时确定球面正交图的可测分数色数（预印本，尚未审稿）
2026-10-20 · arXiv
-
AI 飞跃学科飞跃
On the OpenAI proof that Landau-Siegel zeros do not exist Banks 逐行核验并重写 OpenAI 的“朗道–西格尔零点不存在”证明，给出显式常数（q₀=10¹⁰，δ₀=3.0×10⁻³）AI：OpenAI 模型给出解析数论近百年核心难题的证明（2026-10-01 手稿），密苏里大学 Banks 逐行核验并称论证成立，Kerr 另给出更简证明（arXiv 2610.21099），Lean 形式化经两个独立内核复核；学科：西格尔零点阻碍算术级数素数分布与类数的有效估计，若最终确认将改写多个经典结果（尚未经期刊审稿，陶哲轩称仍在消化）
2026-10-11 · arXiv
-
学科飞跃
An $O(1)$ Bound for the KLS Constant Song 与 Zhang 借助人类主导的 AI 智能体证明 31 年悬而未决的 KLS 猜想（各向同性对数凹测度的 Cheeger 常数有维度无关下界）；Klartag 等三位专家独立给出证明并称其判据为“关键一步”AI：微软研究院称研究者用人类主导的智能体流程探索了 100 多种思路，由人筛选并完成论证（AI 的具体贡献为微软自述，未经独立核实）；学科：KLS 是高维凸几何的核心公开问题（1995 年提出），Bizeul、Klartag、Lehec 于 10-04 独立给出证明（arXiv 2610.05474），Balasubramanian 等另给出显式常数证明（arXiv 2610.07728），并有 Lean 4 形式化；均为预印本，尚未经期刊审稿
2026-10-01 · arXiv
- Mathematical discovery and exploration can be done at scale PNAS 正式发表 AlphaEvolve 数学发现论文（Tao 等）
规模化 AI 数学发现首次通过顶刊同行评审
2026-09-30 · Proceedings of the National Academy of Sciences
- Forbidden Sidon subsets of perfect difference sets, featuring a human-assisted proof PNAS：解决 1000 美元 Erdős 奖金问题，Lean 证明由 ChatGPT 生成
Erdős 奖金问题解答经 PNAS 同行评审发表，Lean 证明由 ChatGPT 生成
2026-05-22 · Proceedings of the National Academy of Sciences
-
AI 飞跃
Advancing Mathematics Research with AI-Driven Formal Proof Search DeepMind 形式化证明搜索智能体在 Lean 中自主解决 353 个公开 Erdős 问题中的 9 个、44/492 个 OEIS 猜想（arXiv 2605.22763）首次大规模评估 AI 在 Lean 中求解公开问题，结果可机器核验，单题成本几百美元
2026-05-21 · arXiv
-
学科飞跃
Remarks on the disproof of the unit distance conjecture 《关于单位距离猜想被推翻的评注》：9 位数学家给出人类核验、简化和推广的证明（arXiv 2605.20695）独立专家核验是把 AI 结果算作数学成果的关键一步；文中指出论证依赖 Ellenberg–Venkatesh、Golod–Shafarevich 等思想
2026-05-20 · arXiv
- Olympiad-level formal mathematical reasoning with reinforcement learning AlphaProof 论文：强化学习实现奥赛级形式化数学推理（Nature）
AlphaProof 方法经同行评审发表，证明强化学习 + Lean 可行
2025-11-12 · Nature
-
AI 飞跃
Mathematical exploration and discovery at scale AlphaEvolve 数学探索论文：67 个问题，多处改进已知最佳构造，11 维接吻数下界 592→593（arXiv 2511.02864）由 Tao 等人联合署名，覆盖分析、组合、几何、数论，把 AI 构造搜索变成规模化方法
2025-11-03 · arXiv
- FrontierMath: A Benchmark for Evaluating Advanced Mathematical Reasoning in AI FrontierMath：由数十位数学家出题的研究级数学基准（Epoch AI）
发布时前沿模型正确率不足 2%，成为衡量 AI 数学研究能力的主要标尺
2024-11-07 · arXiv
- Solving olympiad geometry without human demonstrations AlphaGeometry 达到奥赛几何接近金牌水平（Nature）
奥赛几何接近金牌，但属于竞赛题而非研究问题
2024-01-17 · Nature
-
AI 飞跃
Mathematical discoveries from program search with large language models FunSearch 用大模型找到帽集问题新构造（Nature）LLM 首次在公开数学问题（帽集）上找到超过人类已知最佳的新构造
2023-12-14 · Nature
- Advancing mathematics by guiding human intuition with AI DeepMind 与数学家合作：机器学习引导直觉发现纽结理论与表示论新结果（Nature）
首次在顶刊证明 AI 能帮助数学家提出并证明新定理（纽结不变量关系、Kazhdan–Lusztig 多项式猜想进展）
2021-12-01 · Nature
- Generating conjectures on fundamental constants with the Ramanujan Machine 拉马努金机：算法自动生成基本常数的连分数猜想（Nature）
计算机自动提出数学常数公式猜想，部分后被证明
2021-02-03 · Nature
- Eisenbud–Schreyer–Weyman Ulrich 问题与 Hochster 小 Cohen–Macaulay 猜想反例综述 The recent counterexamples to the Eisenbud-Schreyer-Weyman Ulrich problem (2003) and to Hochster's small Cohen-Macaulay conjecture (1973): a survey, with a generalization to arbitrary dimension
梳理 2026 年 9 月四篇预印本和一份 AI 生成稿件如何把射影几何中的一个数值障碍推进到局部代数，得到两个长期问题的反例，并推广到任意维数。
2026-10-21 · arXiv · Cristian Anghel
- ℝPⁿ⁻¹ 中的正交不等式与“双帽猜想” An orthogonality inequality in $\mathbb{RP}^{n-1}$ and the double-cap conjecture
证明在实射影空间中“帽”使正交邻域测度最小，由此得到双帽猜想：球面上不含正交点对的可测集测度不超过两个半径 π/4 的对顶开帽；主结论另有一份基于不同论证、几乎完全由 AI 工具完成形式化的 Lean 4 证明。
2026-10-20 · arXiv · Allen Ibiapina, Carlos Gomes, Alan Pio, Samuel Belo
- 用机器学习标注的数据训练：随机一阶与零阶优化 Training with ML-labeled Data via Stochastic First- and Zeroth-Order Optimization
针对部分样本有真值标签、其余由机器学习模型标注（可能有错）的数据，提出随机一阶和零阶优化训练方法，实验从线性回归到大模型微调。
2026-10-19 · arXiv · Maria-Eleni Sfyraki, Jun-Kun Wang
- 超越排行榜：面向具体应用的大模型能力画像方法 Beyond Leaderboards: A Method for Application-Specific Capability Profiling of Large Language Models
提出按具体应用评估大模型能力的方法和容器化测试平台，例如数据库迁移智能体和基于文档的聊天机器人，帮助工程师按应用、架构和成本选型。
2026-10-19 · arXiv · Oleg Grynets, Vasyl Lyashkevych, Andrii Salyk, Dmytro Koziuberda
- Rózsa：可认证的等式推理 Rózsa: Certified Equational Reasoning
为 SAIR 数学蒸馏挑战赛第二阶段开发的求解器，判断二元运算集合上一个等式是否蕴含另一个，并把证明或反例转成 Lean 证书；正式评测解出 199/200 题，排名第 6。
2026-10-19 · arXiv · Georgios Kissas
- 用证明论研究证明数据：以 AI 生成的数学为例 Studying proof data with proof theory: the case of AI-generated mathematics
提出一种分析大规模形式化验证证明（如 OpenAI 发布的证明）的方法，把证明项大小、冗余步骤数等量变成衡量 AI 生成数学的指标。
2026-10-18 · arXiv · Safal Raman Aryal
- 带配对辅助观测的高斯过程赌博机 Gaussian Process Bandits with Paired Auxiliary Observations
提出 AI-GPB 方法，在贝叶斯优化中利用事先已有的低成本辅助数据降低观测噪声带来的方差，加快黑箱优化。
2026-10-17 · arXiv · Weibo Huang, Qing Feng, Ruihao Zhu, Cheng Hua
- KLS 常数的 O(1) 上界：证明 Kannan–Lovász–Simonovits 猜想 An $O(1)$ Bound for the KLS Constant
证明各向同性对数凹测度的 Cheeger 常数有与维度无关的下界（ψₙ≤C），从而解决 KLS 猜想，并给出庞加莱常数的普适上界；微软称研究中使用了人类主导的 AI 智能体。
2026-10-01 · arXiv · Zhao Song, Xinzhi Zhang
- 近约 30 天来自 arXiv、bioRxiv、medRxiv、OpenAlex；要点由本站根据摘要撰写。
- Kronecker Delta Rule for Long Context Linear Attention 2026-10-19
- MAI-Gym: An Open All-in-One Platform for GUI Agent Evaluation and RL Training across Mobile and Computer Environments 2026-10-14
- Recovering Reliable Supervision via Critique-Guided On-Policy Distillation 2026-10-14
- TPPO: Tracking-Value PPO For Language Model Reasoning 2026-10-12
- Questioning the Questions: Sustaining Self-Evolution in Reasoning Models 2026-10-03
- Sharpening Tax in Post-Training 2026-10-01
- 在论文归档中查看全部 →
里程碑 24· 9 个飞跃
大号发光节点是飞跃性突破： AI 飞跃 冷色 · 学科飞跃 暖色 · 双环 = 两者都是
-
论文 ⓘ 说明
人类数学家借助 AI 证明“双帽猜想”（球面上无正交点对的集合测度上限），主结论另有几乎完全由 AI 完成形式化的 Lean 4 证明AI：作者在摘要中说明 AI 协助撰写论文，主不等式和双帽结论的另一份 Lean 4 证明几乎完全由 AI 工具完成形式化与验证；学科：双帽猜想是球面上“无正交对集合”测度的长期公开问题，论文同时确定球面正交图的可测分数色数（预印本，尚未审稿）
arXiv预印本 -
科学发现 ⓘ 说明
Quanta：数论专家基本认可 OpenAI 的“准黎曼猜想”证明（零点实部在 1/12 与 11/12 之间），Sarnak 改课专门研读AI：Stanford 的 Lichtman 称其为“迄今最重要的 AI 数学成果”，证明综合了被忽视的亚辛形式等旧工具；学科：Radziwiłł 称黎曼猜想的大部分推论已可由准黎曼猜想推出。证明仍是预印本，人工整理稿尚未发表
Quanta Magazine预印本 -
论文AI 飞跃学科飞跃 ⓘ 说明
Banks 逐行核验并重写 OpenAI 的“朗道–西格尔零点不存在”证明，给出显式常数（q₀=10¹⁰，δ₀=3.0×10⁻³）AI：OpenAI 模型给出解析数论近百年核心难题的证明（2026-10-01 手稿），密苏里大学 Banks 逐行核验并称论证成立，Kerr 另给出更简证明（arXiv 2610.21099），Lean 形式化经两个独立内核复核；学科：西格尔零点阻碍算术级数素数分布与类数的有效估计，若最终确认将改写多个经典结果（尚未经期刊审稿，陶哲轩称仍在消化）
arXiv预印本 -
数据集
OpenAI 在 GitHub 发布 openai/math：719 篇稿件、372 个结果族、约 42% 主结果 Lean 形式化一次性公开 719 篇 AI 数学稿件、约 42% 主结果附 Lean 证明；但出现撤回，数学界有公开抵制
OpenAI厂商自述 -
科学发现学科飞跃 ⓘ 说明
Song 与 Zhang 借助人类主导的 AI 智能体证明 31 年悬而未决的 KLS 猜想（各向同性对数凹测度的 Cheeger 常数有维度无关下界）；Klartag 等三位专家独立给出证明并称其判据为“关键一步”AI：微软研究院称研究者用人类主导的智能体流程探索了 100 多种思路，由人筛选并完成论证（AI 的具体贡献为微软自述，未经独立核实）；学科：KLS 是高维凸几何的核心公开问题（1995 年提出），Bizeul、Klartag、Lehec 于 10-04 独立给出证明（arXiv 2610.05474），Balasubramanian 等另给出显式常数证明（arXiv 2610.07728），并有 Lean 4 形式化；均为预印本，尚未经期刊审稿
arXiv预印本厂商自述 -
竞赛
IMO 2026：AxiomProver 以 Lean 形式化证明拿满分 42/42IMO 2026 满分并公开全部 Lean 证明，可机器核验；但 IMO 官方成绩不含 AI
Axiom Math厂商自述 -
论文
PNAS：解决 1000 美元 Erdős 奖金问题，Lean 证明由 ChatGPT 生成Erdős 奖金问题解答经 PNAS 同行评审发表，Lean 证明由 ChatGPT 生成
PNAS -
论文AI 飞跃 ⓘ 说明
DeepMind 形式化证明搜索智能体在 Lean 中自主解决 353 个公开 Erdős 问题中的 9 个、44/492 个 OEIS 猜想（arXiv 2605.22763）首次大规模评估 AI 在 Lean 中求解公开问题，结果可机器核验，单题成本几百美元
arXiv预印本 -
论文AI 飞跃学科飞跃 ⓘ 说明
单位距离猜想被推翻：OpenAI 通用推理模型构造出 n^{1+ε} 个单位距离的点集，否定 Erdős 1946 年的 n^{1+o(1)} 猜想悬而未决约 80 年、被称为组合几何“最著名的问题”；证明经 Alon、Gowers、Sawin 等 9 位外部数学家核验并写成人类可读版本（arXiv 2605.20695），Sawin 将 ε 改进到 0.014
OpenAI厂商自述 -
论文学科飞跃 ⓘ 说明
《关于单位距离猜想被推翻的评注》：9 位数学家给出人类核验、简化和推广的证明（arXiv 2605.20695）独立专家核验是把 AI 结果算作数学成果的关键一步；文中指出论证依赖 Ellenberg–Venkatesh、Golod–Shafarevich 等思想
arXiv预印本 -
论文AI 飞跃 ⓘ 说明
AlphaEvolve 数学探索论文：67 个问题，多处改进已知最佳构造，11 维接吻数下界 592→593（arXiv 2511.02864）由 Tao 等人联合署名，覆盖分析、组合、几何、数论，把 AI 构造搜索变成规模化方法
arXiv（Georgiev、Gómez-Serrano、Tao、Wagner）预印本 -
竞赛AI 飞跃
Gemini Deep Think 获 IMO 2025 官方评分金牌（35/42）首个经 IMO 官方评分的 AI 金牌（35/42），用自然语言作答
Google DeepMind -
系统发布AI 飞跃
AlphaEvolve 改进 4×4 复矩阵乘法等数十个问题4×4 复矩阵乘法用 48 次乘法，改进 Strassen 1969 年以来的结果；数十个问题追平或超过已知最佳
Google DeepMind -
论文
DeepMind 与数学家合作：机器学习引导直觉发现纽结理论与表示论新结果（Nature）首次在顶刊证明 AI 能帮助数学家提出并证明新定理（纽结不变量关系、Kazhdan–Lusztig 多项式猜想进展）
Nature
这个筛选下没有里程碑。
更多论文与仓库 16
最新新闻 12
- The crisis of AI-generated mathematics
arXiv math.HO 数学史与综述于2026-10-20发布的论文，涉及AI 数学，原题《The crisis of AI-generated mathematics》，详见原文链接。
arXiv math.HOen论文预印本 - Studying proof data with proof theory: the case of AI-generated mathematics
arXiv cs.LO 逻辑与形式化于2026-10-20发布的论文，涉及AI 数学，原题《Studying proof data with proof theory: the case of AI-generated mathematics》，详见原文链接。
arXiv cs.LOen论文预印本 - Formalization of R\'{e}nyi Differential Privacy in Isabelle/HOL (Draft version)
arXiv cs.LO 逻辑与形式化于2026-10-20发布的论文，涉及AI 数学、AI 科研与调研、AI 商业融资，原题《Formalization of R\'{e}nyi Differential Privacy in Isabelle/HOL (Draft version)》，详见原文链接。
arXiv cs.LOen论文预印本 - Simons Foundation Launches $15M Effort To Help Mathematicians Navigate AI Era
Terence Tao 博客于2026-10-16发布的文章，涉及AI 数学、AI 软件开发，原题《Simons Foundation Launches $15M Effort To Help Mathematicians Navigate AI Era》，详见原文链接。
Terence Taoen - Is this the 'mathocalypse'? Why OpenAI's latest results dump has left mathematicians in shock
Phys.org 解读 OpenAI 本周发布的 722 篇数学成果为何让数学家震惊，以及“mathocalypse”说法的由来。
Phys.org Mathematicsen - OpenAI withdraws three preprints a day after releasing 722 manuscripts on unsolved math problems
OpenAI 在 GitHub 上公开 722 篇 AI 生成的数学预印本后不到 24 小时，就因错误撤回其中 3 篇（内容涉数学，与数学组可能重复）。
Retraction Watchen - AHM Statement on OpenAI’s October 6 Release of Mathematical Documents
陶哲轩博客转载“人类数学协会”(AHM)对 OpenAI 10 月 6 日数学文档发布的正式声明。
Terence Tao blogen - Sharing AI progress in mathematics
OpenAI 发布内部前沿模型在数学开放问题上的一批新结果，并在 GitHub 公开 Lean 形式化证明与研究细节（厂商自述）。
OpenAI Newsen - AI just solved an 80-year-old ‘Erdős problem,’ and mathematicians are amazedScientific Americanen