数
← 返回索引

数学

AI4Science 科学领域

按时间汇集该科学领域的研究发布与公开讨论。

最新动态

这是正常的糟糕工作: OpenAI 的数学预印本被批低质

数学家 Sophie Huiberts 在客座文章中主张,证明定理意味着对数学领域负有责任:要说明做了什么、哪些步骤需要新想法、哪些已众所周知,并应更好地阐释重要想法。她把 OpenAI 的行为与此对比:不关心其“预印本”,不适当标注想法来源,把 372 项结果切分成 719 份 PDF,工作含有应被撤稿的错误,承诺代码却未提供,证明极难解析。她称这些 PDF 拖累文献,是内部基准测试的废气,并非“为了科学”;新内部模型或许一键生成文本,但类似结果很快也会由专家发现,部分已由 ChatGPT 用户发现并正在被正式撰写。即便不指控剽窃,科学软件供应商主动抢发客户成果也不好看;专家提示出结果会承担责任,OpenAI 不仅拒绝承担,还阻止客户承担。

查看原文 ↗

OpenAI称未发布模型Astra取得数学与计算机科学十项进展, 生成式AI引发数学界归因与责任讨论

8月,OpenAI宣布,其尚未发布的模型Astra在数学与计算机科学领域取得十项进展,涵盖几何、密码学与编码理论,并发布关于“对数学界的责任”的声明,承认归因、AI辅助结果正确性的问责及数学发现性质变化等关切。ChatGPT、Claude等大语言模型正冲击数学界:院系面临研究与教学中的伦理问题,期刊编辑委员会收到大量AI撰写论文并需决定如何评估与披露生成式AI的使用,arXiv数学投稿近期激增,资助机构开始制定AI使用政策。对于机器能否发现证明、构造例子或提出问题,人类数学创造力是否仍有独特价值,数学重在产出定理还是增进理解,以及贡献如何归属,数学界仍缺乏共识,部分数学家对学科未来感到焦虑。源文本末句中断。

查看原文 ↗

研究者担心成果被AI抢发: Navier–Stokes问题与OpenAI时间点之争

AI智能体自主科研能力提升,研究者担心"会被机器人抢发成果吗":过去五周内至少两次,学者钻研的问题被AI公司抢先作答或宣布结果,有人因此减少使用可能抓取未发表工作的工具。9月7日,纽约大学数学家Tristan Buckmaster称与Anthropic的Levent Alpöge围绕Navier–Stokes问题已推进一年;次日OpenAI宣布其agents解出该难题,Buckmaster质疑该时间点,并怀疑两人上传的信息被用于训练;OpenAI否认,称调查确认其"prompts"不可能以任何方式影响系统。

查看原文 ↗

AgenticBBO-Bench: 跨域评测LLM智能体的黑箱优化能力

黑箱优化(BBO)常见于目标评估昂贵且受限的科学与工程问题。现有LLM智能体结合任务语义、计算、优化工具与反馈决策求解BBO,但任务领域和系统配置不一,结果难以比较。为此,作者提出AgenticBBO-Bench,在统一有限预算协议下覆盖合成函数、超参数优化、数据库调优、芯片设计与分子设计五个领域。实验显示,智能体BBO在全部五个领域族平均得分高于直接LLM方法,并在四个领域优于最佳数值优化器。研究还考察优化工具、任务信息与先验知识、LLM在搜索中的作用三因素:额外数值工具未持续提升性能;任务语义普遍有用,而具体先验较不可靠;数值优化器可吸收智能体搜索轨迹带来的增益。最后,提出五任务前沿挑战,在Codex框架下评估七个LLM,GPT-6 Astra和DeepSeek-V4.1-Flash位于性能与成本的Pareto前沿。

查看原文 ↗

OpenAI 论文探讨 Kohn-Sham DFT: Coulomb 基态密度无系综表示

几天前,OpenAI 发布了一篇由因 Navier-Stokes 而闻名的“内部前沿模型”生成的论文《A Coulomb ground-state density without Kohn-Sham ensemble representation》。帖子称,论文考虑 2 个原子核和 3 个电子的体系,用约 40 页(看似)证明:在“足够大”核间距下,无论有效势如何选择,限制性开壳层系综 KS-DFT 都无法描述其基态密度。发帖者追问“足够大”的含义:定理 2.2 暗示 200 bohr 必要但不充分;定理 1.1 和第 7 节把核间距设为 2×10^200 bohr,比可观测宇宙直径大 10^163 个数量级。他询问这对 DFT 解析基础研究是否重要、论文是否有用于函数不等式的新技巧,以及该下界能否收紧到不涉及星系际尺度。

查看原文 ↗

《The Mathocalypse》: OpenAI 发布 372 项结果, 据称含 Unique Games Conjecture 证明

这篇个人记述称,昨日 OpenAI 发布了 372 项重大结果,其中包括在 Timothy Gowers、Edward Witten 等数学家推荐下给出的 Subhash Khot 的 Unique Games Conjecture(UGC)证明;若成立,许多优化问题即便只求略优于半正定规划松弛的近似也属 NP-hard。作者强调目前只是“相当确信”它是证明:部分结果有 Lean 证书,并非全部;似乎还没有人类理解这些证明,验证竞赛才刚开始。Dana Moshkovitz 形容论文极难读、需 AI 辅助,UGC 证明发明了带噪声测试的怪异递归码,既非长码也非短码;另有绕过 UGC 的 Max Cut 与所有 CSP 的最优 NP 硬度近似证明。

查看原文 ↗

Gary Marcus 评论 OpenAI 数学大发布: 报告含糊, 泛化性无从判断

Gary Marcus 在这篇仓促写就的评论中指出,OpenAI 新发布的数学成果真正的新闻不在于结果,而在于对外说明的含糊:所谓“相同流程”“使用一个未公开模型”的说法无法通过同行评审,外界无从知道证明是一次性生成再由符号系统 Lean 验证,还是经过迭代过程,也不知道失败率、训练、后训练与数据增强的情况。因此,他对该成果在数学之外有多强的泛化能力毫无概念。他批评社交媒体讨论已沦为不明就里的欢呼,认为新系统既可能是迈向 AGI 的一步,也可能只是在可验证领域对 Lean 与合成数据的巧妙利用、毫无通用性;仅凭初步报告几乎看不出任何东西。

查看原文 ↗

OpenAI发布722篇AI生成数学手稿, 验证问题引争议

OpenAI发布了一批由其内部前沿模型生成的722篇数学手稿,涵盖数学与理论计算机科学领域的数百个研究问题,整理为372组相关成果,包含证明、替代论证、推论与支撑材料,其中不少结果附有Lean形式化证明。OpenAI表示,在现有数学评测表现开始趋于平台期后,团队把内部模型用于开放研究问题,评测过程约向模型提出4000道题;平均每项结果所用算力约相当于ChatGPT Pro思考三小时。公司同时强调,发布并不意味着所有结果都已完全验证,仓库中成果处于不同检查阶段,部分尚未在Lean中形式化的手稿可能含有错误;更正与修订会被记录,旧版本仍会保留。

查看原文 ↗

OpenAI一次公开722篇数学手稿: 准黎曼、BSD、霍奇等三大千禧难题在列

OpenAI一夜甩出722篇数学论文!黎曼霍奇BSD全上阵,数学家:读不过来 三位菲尔兹奖得主:不代表认可 听雨 发自 凹非寺 量子位 | 公众号 QbitAI 刚刚,OpenAI往数学界扔了颗重磅炸弹—— 一口气公开722篇数学手稿,全部出自一个还没发布的内部模型。 这些手稿归成372组结果。据OpenAI介绍,模型此前一共尝试了约4000个研究问题,平均每项结果消耗的算力,约相当于ChatGPT Pro思考3小时。 论文、源码、部分Lean证明,被一股脑传上了GitHub。 翻开目录,准黎曼猜想、霍奇猜想、BSD猜想、π的无理性指数……一个比一个名头大。 光是千禧难题,就沾上了三道。 再往下翻,还有自旋玻璃、量子磁性、自由群因子、相对论性弗拉索夫—麦克斯韦方程……数论、代数几何、理论计算机、统计力学,17个方向铺得满满当当。 一夜之间,数学论文堆成了山。 数学家们看了直呼:这谁读得完啊…… 722篇手稿里,究竟写了什么? 点

查看原文 ↗

OpenAI 公开未发布内部模型产出的 722 篇数学手稿

OpenAI 在 2026 年 10 月 6 日的研究文章中宣布,将一个尚未发布的内部前沿模型产出的数学成果公开:openai/math 仓库以 Apache-2.0 许可发布 722 篇手稿,归入 372 个家族,并附 Lean 形式化证明与模型推理摘要。README 称绝大多数结果由同一套流程产生,评估过程中模型被给出约 4,000 道问题,平均成果所用算力约相当于三小时 ChatGPT Pro 的思考。并非所有手稿都配有 Lean 形式化,README 提醒部分未形式化结果可能存在问题,OpenAI 表示会尽快修正并保留公开发布历史。

查看原文 ↗

OpenAI一次公开372项数学成果, 学界要求先拿出证据

OpenAI在GitHub上公布其新模型产生的372项成果,称每一项都解决或大幅推进了数学或理论计算机科学中的重大公开问题,其中包括四维Kakeya猜想的解法、对部分重要计算机算法的改进,以及朝Riemann猜想的实际进展。许多结果已在Lean(可校验证明逻辑的编程语言)中通过验证。OpenAI发言人告诉《Scientific American》,这款尚未公开的模型几乎所有结果都是对单个AI智能体的一个提示词作答所得;这与此前Navier-Stokes问题的解法不同——后者由一万个智能体组成的群体协作完成,耗费数百万美元算力。麻省理工学院数学家Andrew Sutherland表示,在OpenAI发布模型、结果可被复现之前,应把

查看原文 ↗

Hexagon: 面向数学与理论计算机科学的新论文仓库启动

Hexagon 是面向数学与理论计算机科学的新论文仓库,由多人自 2026 年 8 月初起合作筹建。作者认为借助 LLM 证明的结果大量涌现,需要新的收集模式:成果可被引用、可长期可靠保存,作者与社区参与门槛低于 arXiv,并为这些工作提供区别于 GitHub 仓库或 X/Bluesky/Mathstodon/LinkedIn 帖文的归属地。为支持项目,团队在特拉华州成立 Hexagon Mathematics Foundation,并拟申请 501(c)(3) 免税资格,作者出任首任执行主任。他举例说,与 FRG 资助团队合作时点击按钮即得到特征零四重子 Hodge 数的导出不变性这一新结果,他不愿署名而只在博客披露,如今该结果以 hexagon:2609.00104 收录于 Hexagon。

查看原文 ↗

Erdős problems网站创办人Thomas Bloom谈AI冲击下的收获与隐忧

Thomas Bloom在Erdős problems网站的公告中写道,建站本意是面向人类读者推介这些问题、梳理已有工作,却意外成为衡量AI能力的风向标:近一年来AI从几乎无用变为可帮助解决部分最难的数学问题,他也坦承不少近期进展其实来自人力投入增加与重新关注。负面效应包括:有人把Erdős风格数学贬为'简单/消遣',有人因自认无法与AI竞争而放弃思考,更出现大批缺乏解释的AI解答,挤占并打击真正有兴趣的人。数周前他征集改版意见,收到公开与私下反馈,其中不少受益者从未留言。

查看原文 ↗

陶哲轩在SAIR演讲中呼吁AI数学研究慢下来, 警告“证明消化不良”

不er,咋陶哲轩也成AI减速派了?? Jay 发自 凹非寺 量子位 | 公众号 QbitAI 不er,陶哲轩咋成AI减速派了?? 是的,就是那个曾经最爱AI、逢人就安利AI工具的男人,一夜之间,漂移到了AI数学的对立面。。。 SAIR最新演讲,陶哲轩正式向模型公司开火: 简直是疯了,AI公司无休止地加速,却对那之后会发生什么一无所知。 必须慢下来。完全没理由这么快,一点理由都没有。 更关键的是,感受到危机的,远不止陶哲轩一人。 而且陶哲轩还算反应比较淡定的。 你的菲尔兹奖得主Cédric Villani,在看到OpenAI拿下千禧难题后,直接瘫软了。。。 我大受震撼…… 简直跟世界末日一样,这是数学界有史以来从未见过的浩劫。 但我往前翻了下发现,仅仅在3个月前,这哥们对AI的态度还是嗤之以鼻啊。 LLM根本没有智能,连洗车问题都会答错,只不过是统计学复读机。 洪水是一视同仁的。 面对光速迭代的大模型,即便站在人类智能金字塔尖的天

查看原文 ↗

Sherpa: 让大模型教师按学生偏好调整教学的多轮强化学习框架

现有训练大模型当教师的方法依赖示范数据、偏好数据或预设教学标准,往往与学生个人的学习效果脱节。研究提出多轮强化学习框架 Sherpa:用大模型模拟出具有不同学习偏好的学生原型,让教师模型直接以最大化学生学习效果为目标来调整讲授方式。结果显示,经 Sherpa 训练的教师使所有原型学生的成绩平均提高 20.5 个百分点;在 MathTutorBench 评估中,整体教学分数由 52.5% 升至 79.2%;人工评测里,79.6% 的成对比较中受训教师比基座模型更受青睐。

查看原文 ↗

OpenAI宣称攻克Navier-Stokes问题,数学界在海德堡论坛展开审视

9月13日,德国海德堡Heidelberg Laureate Forum上,学者热议OpenAI、Anthropic、Google等AI公司进入数学。AI已解出Erdős的系列征题、验证Fermat大定理证明,最近OpenAI宣布解决Navier-Stokes存在性与光滑性问题——Clay Mathematics Institute于2000年提出的七个Millennium Prize Problems之一;此前仅Poincaré猜想由人类解决,若经验证将成为自动推理的分水岭。多伦多大学Fields奖得主Jacob Tsimerman称能力提升快于预期,“解决Navier-Stokes感觉相当确凿”,但他不了解细节;阿姆斯特丹大学Ailsa Robertson说“AI和LLM今夏点燃了数学界”。

查看原文 ↗

OPPD: 序列级幂分布的在策略蒸馏, 一次生成即获锐化收益

语言模型给正确答案的概率虽高于任一单个错误答案,却仍常采到错误答案。OPPD 让被训练模型生成候选,用冻结教师的幂分布以序贯蒙特卡洛加权,并以同一权重做最大似然更新,使模型一次生成即获得锐化效果。训练后单次生成较未训练模型同温度在 MATH500、GSM8K 最高分别提升 23.0、27.3 分,比 64 候选的已发表幂采样高 2.4、3.5 分,找回 16 候选所给增益的 94%。相较同检查点、同预算的 GRPO,OPPD 在 MATH500、GSM8K、AIME 分别高 3.8、4.0、5.4 分且不用参考答案;GRPO 之后再做最多再加 9.3 分。仅以数学训练也使 HumanEval 最高升 5.3 分。

查看原文 ↗

不可压缩流体方程的经典解与有限时间奇点

Euler 在1757年的备忘录中提出无粘不可压缩流体方程,距今已超过250年,是数学物理中最早的偏微分方程组之一。核心问题是初始光滑的流体运动是否会在有限时间内形成奇点;借助大语言模型对 Euler 与 Navier–Stokes 方程的近期研究使这一问题重新受到关注。本文回顾相关数学进展,包括在局部存在与唯一性框架内构造有限时间产生奇点的经典解,以及通过涡层级联构造爆破解的思路,并以 Riccati 方程为例说明解如何在有限时刻变得无界。

查看原文 ↗

DiffGate: 按难度门控教师引导的在策略蒸馏目标

现有在策略蒸馏(OPD)目标多为逐 token 判别、忽视结果,而基于可验证奖励的强化学习(RLVR),尤其是 GRPO,能提供结果级监督,却面临奖励稀疏、信用分配粗糙、在全部失败的组上奖励消失等问题。作者提出 DiffGate:由验证器决定哪些轨迹接受教师引导——仅对失败轨迹施加教师监督,按组难度缩放,并平滑限幅,避免极端师生差异主导优化。在 Qwen3-0.6B 与 Qwen3-1.7B 学生模型上,代码 avg@8 较匹配的 GRPO 分别提升 1.7 与 1.8 分,pass@8 提升 1.6 与 5.7 分;数学 avg@8 与 GRPO 相差 0.5 分以内,pass@8 提升 1.1 与 3.9 分,四个模型-领域设置的 pass@8 均有改善。

查看原文 ↗

大语言模型背后的数值线性代数

这是一篇以机器学习技术、特别是大语言模型(LLM)为重点的综述文章。文章回顾了数值线性代数的历史作用:1950至1960年代,空气动力学中特征值问题的研究催生了LR和QR算法,随后注意力转向稀疏线性方程组求解。作者指出,当前机器学习浪潮对科学与工程具有颠覆性影响,LLM等工具建立在矩阵与张量方法之上,并认为随着我们接近通用人工智能(AGI),矩阵方法将发挥更重要作用,而变革的速度对数值线性代数从业者尤为挑战。文章有两大目标:一是向数值方法专家清楚阐释大语言模型的核心概念;二是梳理LLM技术所使用的关键数值线性代数概念,并介绍NLA近期对该领域的若干重要贡献。

查看原文 ↗

Meta AI 与数学家合作, 用 Muse Spark 产出六篇研究论文

Meta AI 宣布与数学家合作完成六篇论文,其中五篇给出此前未决研究问题的答案。研究者在 meta.ai 常规聊天界面中使用 Muse Spark 1.1 与 1.2 的 Thinking Mode,未借助定制研究脚手架。合作遵循几项原则:数学家团队主导探索并发展论证,第二组数学家复核,论文标明哪些段落主要由研究者撰写、哪些由 AI 起草,并注明所基于的前人研究与数学思想。Meta 表示,工作完成后获悉 Meta 之外的团队已用不同方法独立宣布解决了其中部分问题,论文中已致谢并说明其与本文的关系。首篇为概率领域论文 The Strict Threshold for Gaussian Ellipsoid Fitting。

查看原文 ↗

Pivot-SD: 面向掩码扩散语言模型的高效自蒸馏方法

掩码扩散语言模型(dLMs)为复杂推理提供了可并行的自回归替代方案,但存在信用分配难题:去噪过程中的少数几步承诺会大幅削减其余掩码位置的不确定性,并主导整个回答。现有后训练方案多在最终文本上训练,或把奖励归到整个去噪步骤,而不会挑选具体承诺。Pivot-SD 是一种高效离线自蒸馏框架,用信息增益指标衡量对剩余掩码位置的不确定性削减,只监督这些高影响的“枢轴”(pivots):成功轨迹的枢轴用交叉熵训练,失败轨迹的枢轴用针对性的非似然训练,失败轨迹其余部分保持不动。仅用 200 个问题、每个 4 次采样,Pivot-SD 在数学与代码基准上均优于全序列 SFT 和预算相当的扩散 RL 基线,提升了 LLaDA-8B-Instruct。

查看原文 ↗

OpenAI研究员Noam Brown谈多智能体: 解千禧年难题中10000个Agent最多占10%功劳

程浅 发自 凹非寺 量子位 | 公众号QbitAI “Navier–Stokes千禧年难题的突破,10000个Agent最多占了10%的功劳。” 此判断出自OpenAI研究员,o1核心作者NoamBrown之口。 NoamBrown,人称“OpenAI推理教父”。在几乎所有人还在卷模型参数的2023年,他就已经开始押注test-time compute scaling(推理时计算) 。 一年后,o1-preview横空出世、震动行业。如今,TTS早已成为行业共识,成了人手一个的“深度思考”按钮。 现在,NoamBrown又带来了他目前的研究方向——多智能体(multi-Agent)系统。 此前,OpenAI发动了10000个Agent,耗时88小时,输出1300亿token,拿下千禧年数学难题。 关于此事,NoamBrown在最新播客中从多智能体系统聊起,深入到了公司经营、RSI发展、超级对齐等领域…… 一个个问题也接连浮现:

查看原文 ↗

Caltech 学者联合声明: Mathathon 改版为 Old Problems, New Proofs

Caltech 数学家联盟发表联合声明,重新设计 Mathathon 活动,新主题定为 Old Problems, New Proofs。发起者认为解题只是数学的一个组成部分,数学理解与阐释同样有意义,却常被资助方和招聘委员会忽视。参与者须挑选一个解答反直觉的问题(如四色定理、ABC 猜想、Navier-Stokes 问题),在 40 小时内尽可能深入学习并向同伴汇报,随后用两个月发展替代理证或阐释,提交 explainer 与 GitHub 仓库,公开 LLM 对话记录、可视化代码等材料。声明强调 Mathathon 把 AI 视为数学家可用的众多工具之一。

查看原文 ↗

在线策略还是离线策略?蒸馏动态的系统研究

在线策略学习常被指能减少灾难性遗忘、让参数更新更稀疏并提升泛化,但以往监督微调与强化学习的比较同时改动诸多因素,难以分离 rollout 策略的作用。该研究在受控强到弱蒸馏中独立改变 rollout 策略、token 级 KL 方向与学习率,覆盖 Llama3 与 Qwen2.5 模型家族及科学、医学、算术推理任务。结果显示 rollout 策略未必起核心作用:KL 方向更明显影响任务表现与输出覆盖,学习率主导遗忘与更新稀疏性。梯度分析及连续学生—教师策略谱实验表明,前向 KL 对策略变化稳健,反向 KL 更敏感且偏好学生 rollout。在线数据能提升 Countdown 更难变体的泛化,但后续 RLVR 后优势不再稳定保持;去掉梯度裁剪、采样 KL 估计和更长推理链任务时结论仍稳健。

查看原文 ↗

LANTERN: 发掘语言模型中隐藏的数学知识

语言模型如今已能证明定理,但研究者仍决定优先探索哪些问题。作者提出 LANTERN——一条快速且低成本的流程:先用基于预训练模型激活值的分类器为候选关系排序,再经分阶段过滤、假设生成、可执行验证与解析检查。应用于整数数列百科全书(OEIS)后,LANTERN 对 10,000 条常被引用的数列之间 5000 万对组合进行排序,产出 62 条彼此尚无 OEIS 交叉引用的数列对之间的已验证关系。经内容筛后保留 13 条值得呈现的关系,其中 9 条具有信息量或洞见,包括据作者所知完全新颖的 4 条——均未出现在 OEIS 或定向文献检索中。含分类器训练、候选排序、过滤与验证在内的端到端流程耗时不足 8 小时。

查看原文 ↗

Tapio Schneider: AI证明之外, 数学与科学更需要理解与信任

Tapio Schneider撰文讨论AI在数学、科学与工程中的角色。OpenAI于9月8日宣布的强迫Navier–Stokes方程有限时间爆破解,由约10,000个AI智能体并行探索生成,随后在Lean中形式化并验证;形式化验证支持其正确性,但数学界仍在消化。陶哲轩等人认为,证明的意义不止于判定命题真假,还在于推进对形状、数字与自然现象基本结构的概念性理解;Yehuda Rav说“定理是标题,证明是内情”。Timothy Gowers指出AI生成的证明行文欠佳很可能只是暂时困扰。作者主张,自然科学与工程同理:episteme(解释性理解)本身即目标,techne(预测与制作的技艺)在预测可被检验时可独立成立——黑箱AI天气模型因预报每天可核对而可信——并可反过来作为服务于理解的工具,例如AlphaFold预测3D蛋白质结构(原文此处截断)。

查看原文 ↗

Navier-Stokes 难题: 数学家质疑 OpenAI 的证明求解了哪个变体

两周前,OpenAI 宣称解决了 Navier-Stokes 这一数学难题,可获 Clay 数学研究所 100 万美元悬赏。但其由内部大语言模型生成的证明被许多专家认为不自然:它求解的是一个被数学家视为脱离现实的变体问题,相当于钻了题目表述的漏洞。方程中外部作用力(如重力)一项可有可无;芝加哥大学 Luis Silvestre 称:“Clay 问题已了结,但 Navier-Stokes 方程的主要问题仍未解决。”上周四,三位数学家给出证明,显示 OpenAI 的方法永远无法推广到完整问题,除非出现全新的思路。

查看原文 ↗

SAIR 推进面向数学社区的开放模型计划

陶哲轩与私人捐赠者共同创立非营利机构 Foundation for Science and AI Research(SAIR),支持 AI 在数学及其他科学中的负责任使用,独立于主要 AI 公司。初期资源有限,活动以播客、短会活动和竞赛为主;近期获 XTX Markets 与 Susquehanna 支持,用于资助下一轮 SAIR 竞赛。SAIR 正与学界、业界多个关键伙伴推进共建开放权重科学模型,以及面向科学应用使用开源与闭源 LLM 的开源工具。因当前局势与对开放模型的高需求,计划提前宣布,部分关键规划仍在进行中;目前正征集可提供资金、算力、专业知识或社区建设的伙伴意向,并提出共建 Math 2.0。

查看原文 ↗

OpenAI宣称用AI攻克Navier–Stokes问题, 成果署名引争议

OpenAI于9月8日宣布其AI模型解决了流体力学难题Navier–Stokes问题,称这或将永久改变数学研究方式,同时引发成果归属争议。纽约大学Tristan Buckmaster与哈佛大学Levent Alpöge此前正借助OpenAI、Anthropic工具攻关该问题,Buckmaster称该公司在听闻其工作后介入,模型或从他们与ChatGPT的交互中学习;OpenAI发言人向Nature表示,经调查可完全确信7月3日后的用户输入不会以任何方式影响该系统,公司9月1日才开始研究,此前未以任何途径看到二人公开前的工作。伦敦政治经济学院知识产权法学者Luke McDonagh提醒,研究者未必意识到向个人AI账户上传数据的后果;25位Fields Medal得主在公开信中称AI工具模糊了恰当署名能力,引发严重的归属与抄袭问题,训练信息难溯源或危及学术信用。

查看原文 ↗

When2Think: 面向混合推理模型的难度感知长度控制后训练框架

大型推理模型(LRM)在复杂任务上表现强劲,却存在系统性低效:常在简单问题上过度推理、在难题上推理不足;而统一长度惩罚或刚性路由等现有方法会带来效率代价,以简单样本的算力削减换取难题上的准确率损失。作者将高效推理表述为实例自适应的算力分配问题,提出后训练框架 When2Think,其核心是实例级难度感知控制(IDAC):利用预计算的参考统计(准确率与 token 用量)塑造奖励,配合基于验证器的奖励与批内标准化优势,实现无需奖励模型或在线参考模型查询的稳定无批评者优化。实验显示,AIME24 上 Pass@3 提升 10.0%、token 用量相对基线降低 27.9%;AIME25 上 Pass@3 达 40.0%,优于压缩与仅路由基线。

查看原文 ↗

特权信息为在线策略自蒸馏(OPSD)增添了什么?

为厘清特权信息对在线策略自蒸馏(OPSD)的独立贡献,构建 AMPLE-Math:含 5,319 道数学题、每题六种共享同一答案的推理视图,并与匹配的无参考蒸馏比较。启用思考的教师监督直接回答式 rollout 时,无参考蒸馏解释了 Qwen3-1.7B 在思考启用评估下的大部分提升,领域内外皆然。Qwen 中额外参考收益证据有限,精修解答最强;SmolLM3-3B 第 50 步完整轨迹提升两个百分点,收益取决于学生。同检查点下,把短直接回答 rollout 换成启用思考的长 rollout,在问题、参考和评估不变时,两模型家族均由增益转为损失。Qwen 的教师画像与匹配损失干预显示,改变 token 级监督可基本不改变学生行为。提示 OPSD 或许通过两种推理模式共享的参数改善既有推理能力的调用;特权参考的价值在于跨模式迁移增益,而非揭示多少解答。

查看原文 ↗

《OpenAI 88小时生成的Navier-Stokes证明: 正确与被理解之间的差距》

9月8日,OpenAI称1万个智能体运行88小时,产出166页的Navier-Stokes方程证明;该问题自1934年悬而未决,属Clay研究所七大Millennium Prize Problem之一,每题100万美元、迄今仅一题颁奖。OpenAI不领奖,外界估算算力账单为1000万至4000万美元。Clay称问题“显然已解决”,但评审“刻意不慌不忙”:证明须在权威期刊发表并经两年检验,官网现标为“Active”。9月11日,25位Fields奖得主签署宣言,批评AI实验室的做法损害数学;次日陶哲轩邀请Silvia De Toffoli与Eamon Duede撰文,区分可由机器验证的逻辑证明与人类可解释、可延展的可理解证明,指出AI使二者分离,并评价OpenAI“给出的是答案,未必是果实……”

查看原文 ↗

前OpenAI后训练VP回应陶哲轩: 别用今天AI的能力框定未来数学

前OpenAI后训练VP回应陶哲轩:说AI毁了数学,可能还是太小瞧AI了 未来的AI不仅能解决问题,还能提出有价值的洞见、建立新的概念框架,让数学家在此基础上继续探索。 henry 发自 凹非寺 量子位 | 公众号 QbitAI 说AI毁了数学,可能还是太小瞧AI了。 刚刚,OpenAI前后训练VPLiam Fedus,回应了陶哲轩等数学家关于“AI不应只追求解题,更应推动数学理解”的观点。 他赞同陶哲轩对概念理解的重视,但也认为不能用今天AI的能力边界,框定未来的可能性。 在Liam看来,未来的AI不仅能解决问题,还能提出有价值的洞见、建立新的概念框架,让数学家在此基础上继续探索。 换句话说,如果AI的训练目标不只是“把题做对”,而是进一步扩展到解释为什么、提炼方法、帮助人类理解,那么它最终可能成为一个既能给答案,也能创造新思路的数学研究伙伴。 这份乐观,与陶哲轩等25位菲尔兹奖得主最初联署的声明,既有共识,也有分歧。 双方都

查看原文 ↗

AI解答数学难题之后, 数学究竟追求什么

一篇客座文章称,OpenAI于2026年9月8日宣布,已生成纳维—斯托克斯存在性与光滑性问题的AI解答;这一宣布引发了关于成果归属及人机各自贡献的争论。参与该事件的一位数学家Tristan Buckmaster将其比作“Deep Blue–Kasparov moment”。作者讨论由此而来的疑问:若AI能回答数学前沿最困难的问题,数学是否会像棋类一样被“解决”。文章认为,“继续玩”强调过程价值虽有道理,但不必把数学视为游戏;“AI已经解决数学”的说法依赖两项前提:AI确实解决了一个数学问题,以及数学只关乎解题,而作者认为这两项前提都不正确。

查看原文 ↗

“幼稚的操场吹嘘”: OpenAI称最新AI模型破解一项Millennium Prize Problem, 数学家感到不安

OpenAI宣称其最新AI模型攻破了一项“Millennium Prize Problem”;该难题悬赏100万美元,数十年来难倒人类。按《卫报》报道,这家估值近万亿美元的私营公司动用了1万个可自主执行任务的AI代理,估算花费1500万美元。数学家既震惊又不安:他们担心进行中的工作被他人抢先吞掉,也担心一键解题时如何培养下一代。圣安德鲁斯大学纯数学负责人Colva Roney-Dougal称自己“有点不知所措”,三个月前还认为AI短期内难有显著突破;曼彻斯特大学David Silvester说领域“非常不稳定”,认为只要有足够资源,所有开放数学问题都可能被攻下;沃里克大学James Robinson则批评大科技公司为炫耀最新模型而烧掉难题燃料,像“幼稚的操场吹嘘”。源文本在最后一句引文处截断,且未提供独立验证或技术细节。

查看原文 ↗

GPT-6 Astra解出FrontierMath Tier 4最后一题, Epoch AI宣布该层饱和

AI数学的最后一道高墙,塌了!GPT-6 Astra刷穿FrontierMath Tier 4 FrontierMath Tier 4,饱和了 henry 发自 凹非寺 量子位 | 公众号 QbitAI 刚刚,最后一道FrontierMath Tier 4难题,被GPT-6 Astra攻破了。 至此,这套曾经被视作大模型数学噩梦的研究级测试,所有题目都已经至少被AI成功解出过一次。 Epoch AI也正式给它下了结论,FrontierMath Tier 4,饱和了。 虽然从上面的图里看,Astra还没有直接干到100%,OpenAI自己公布的成绩也是97.6%。 但按照Epoch的算法,“全部解出”指的是把不同模型、不同时间的尝试累积起来以后,Tier 4里的每一道题都已经有过成功解答。 而Astra干掉的,正是此前唯一还没有被AI攻破的那一道。 (简单理解就是Astra可能在某次测试中出错了,但它对的那道题是此前没被解出来的)

查看原文 ↗

陶哲轩、邓煜等25位菲尔兹奖得主联名声明: AI解题与数学共同体目标严重错位

陶哲轩邓煜究竟在反对什么:AI暴力解题摧毁人类数学精神 25位菲尔兹奖得主联名吹哨 衡宇 发自 凹非寺 量子位 | 公众号 QbitAI 面对近期AI大厂推进数学研究的方式,连一向与AI为善的陶哲轩都坐不住了。 刚刚,陶哲轩、邓煜等25位菲尔兹奖得主联合发起并作为首批签署人,发布了一份声明表示:AI公司推进数学的方式,已经与数学共同体的目标出现“severe misalignment(严重偏移)”。 因鉴于近期AI急剧发展对数学领域带来的冲击极为严峻,发起人未走流程繁琐的协商程序,而是选择紧急公开发布,以尽快回应危机。 过去几个月,大语言模型的数学能力急剧提升,已经能解决多个数学领域中重大的未决问题;但AI公司越来越倾向于把解决数学问题当作benchmark来推进的做法,对数学这门科学、对数学共同体都是有害的。 AI公司的目标与数学共同体的目标严重错位。 我们认为,这属于更广泛的错位问题的一部分,影响着其他科学与创意职业,乃至整

查看原文 ↗

SAIR 发起 Andrews–Curtis 猜想挑战赛

SAIR Foundation 与加州理工学院 Math-AI 团队合作,由 Sergei Gukov、Terence Tao 和 Lucas Fagan 组织的 Andrews–Curtis 猜想挑战赛今日开放。该猜想是组合群论的重要开放问题,并与低维拓扑、奇异光滑四球面、光滑四维 Poincaré 猜想及 Generalized Property R 猜想相关;其解可写成易于验证的组合搜索问题。参赛者需通过 AC1 反转、AC2 相乘、AC3 共轭等不改变底层群的移动,把平衡表示化为平凡表示。Caltech 此前用强化学习和组合搜索处理潜在反例,但许多重要情形仍无进展;组织者希望借助近期 AI 进展解决或证伪该猜想。最著名的 Akbulut–Kirby 族中,AC-平凡性仍开放。

查看原文 ↗

OpenAI 宣称破解 Navier-Stokes 问题, 数据隐私争议随之而来

据 The Week 报道,OpenAI 称用内部模型在约三天内给出 Navier-Stokes 存在性与光滑性问题的证明。该问题属于七大 Millennium Prize Problem,研究描述液体与气体运动的方程,可用于预测天气、模拟洋流或整体气候。New Scientist 称公司先用 1,000 个 AI agent 攻克类似问题,再用约 10,000 个完成任务;客户运行同一问题约需 1,500 万美元(1,100 万英镑)。但成果被一场“争议”笼罩:纽约大学数学家 Tristan Buckmaster 与 Anthropic 研究者 Levent Alpöge 此前也借助包括 OpenAI Codex 在内的大语言模型宣布“破解”三个相关问题,信息私下保存,公布时间在 OpenAI 发布前数小时,由此引发对数据隐私与研究完整性的质疑。

查看原文 ↗

MoE强化学习中的专家空间探索: 显式利用路由结构提升rollout多样性

研究提出 Expert-Space Exploration Reinforcement Learning (ESRL) 框架,在MoE模型的强化学习后训练中显式探索专家路由空间。经验分析显示,扰动专家路由能改变模型输出、增加rollout多样性,效果类似提高解码温度;但直接扰动会激活不合适的专家,显著降低rollout质量。ESRL保留高置信专家作为锚点,将随机路由限制在合理的候选池内,并依据router熵调整扰动强度以避免过度扰动;同时记录rollout阶段使用的专家路径,在策略优化时回放,以缓解扰动带来的路由不匹配。实验表明,ESRL在top-K、top-1、共享专家路由的MoE骨干,以及数学、科学、代码任务上均取得最佳表现,且无需额外采样或计算开销;其中在Qwen3-30B-A3B上较GRPO的平均Pass@1与Pass@8分别提升3.2和4.5个百分点。

查看原文 ↗

Never Give Up (NGU): 用自适应采样缓解RL训练LLM的“马太效应”

研究发现,用RL训练LLM的收益在数据集上并不均衡:模型本来擅长的简单题提升明显,困难题提升有限,作者称之为RL for LLMs中的“马太效应”。其解释是困难题需要更多算力才能找到解,而现代RL方法在简单题上浪费了过多算力,应当动态重新分配算力。为此提出简单自适应采样方法Never Give Up (NGU):对一个问题持续采样直到得到正确答案,结合异步RL,自然地用更少样本筛除简单题,把更多算力分配给难题。文中还考察了off-policy鲁棒性等影响NGU的设计选择,并总结了一组最佳实践。在数学基准Deepscaler上,NGU提升了单位算力的性能,在更难的问题上尤其明显;在编码任务Manufactoria上,带逐测试奖励的标准GRPO无法完全解出难易测试混杂的题目,而NGU不断迭代,逐步攻克更难的测试,最终学会完整解决编码问题。

查看原文 ↗

《MInTRL》: 以最小干预扩展在策略强化学习的探索边界

面向可验证奖励的强化学习通常采用在策略方式,探索局限于策略自身能发现的轨迹;离策略方法可利用外部知识,却可能带来较大的分布偏移。MInTRL 在基本保持在策略的采样中引入稀疏、局部的干预:生成阶段由 judge-intervention 策略定期检查当前策略输出,用简短纠正替换错误后缀后立即交还控制权;训练阶段采用序列级优势回归目标,从而无需重要性采样。作者称,稀疏局部干预在有限预算的在策略采样之外显著提升覆盖度,同时保持轨迹整体的在策略性质。在数学与代码基准上,MInTRL 稳定优于标准在策略与离策略基线;消融实验显示其在自干预和不同 judge 策略下依然有效,且干预强度适中时性能最佳,说明干预应保持最小化。

查看原文 ↗

R^3中无外力Euler方程稳定奇点的自相似研究

Anima Anandkumar介绍其团队针对无外力Euler方程奇点开放问题的工作,并称已将论文和代码公开。该研究不同于NYU团队和OpenAI所采用的具有离散尺度跳跃的多尺度构造,而是尝试为自由空间中的Euler方程寻找自相似奇异剖面。作者称,带边界的Euler方程等修正情形已有成功结果,但边界用于约束奇点的技术不适用于自由空间。团队使用物理信息神经网络(PINN)寻找候选解;此前相关尝试未成功,主要困难包括优化易收敛到平凡解,以及数值精度需足以将数值解转化为解析证明。

查看原文 ↗

GenV: 为自动形式化引入生成式验证, 超越求解器判定

研究指出,符号系统依赖数学求解器保证推理正确性,却无法判断形式化翻译是否与指定的形式化保持严格等价。作者将此漏洞形式化为“判定保持性不忠实”(Verdict-Preserving-Unfaithfulness, VPU):错误编码仍能成功执行并得到预期判定;并从理论上证明,仅依赖判定的结构性验证启发式在这类“看似有效”的轨迹上,检测能力在数学上被限制在随机水平。为此提出生成式验证 GenV,将离线 Z3 等价预言蒸馏为与参考无关的连续参考等价分数,复用语言模型原生词表空间。经决策投影 logit lens 与稀疏自编码器的机制分析显示,该生成式读出无需显式定位训练即可提取精确的误差坐标。其预言挖掘的验证器 GenV+HN 在参考等价验证上达到 0.961 AUROC,能对未见过的翻译器和不同的形式风格零样本泛化,并在 agentic 测试时算力分配中带来 11.3 个百分点的下游准确率提升。

查看原文 ↗

OpenAI 关联账号称约万名 agent 协作取得 Navier–Stokes 奇点相关结果, 引发技术兴趣与质疑

多个与 OpenAI 有关的账号表示,一项 AI 辅助工作得到了 Navier–Stokes 相关结果,讨论聚焦于有限时间奇点(blow-up)。Ethan Knight 称该结果出自约 10,000 个 agent 的协作,OpenAI 过去一年用 multiagent RL 训练模型协同;原标题进一步给出 88 小时、约 130B tokens(逾 4000 万美元)与 Astra-next,并将其称为第二个 Millennium Prize 的有力候选。舆论反应分裂为技术兴趣、质疑与 meta 层面的作者归属争议;有讽刺性转述把数学界接受称作“小形式”。编辑建议不必深究 drama,认为 OpenAI 的成就为真、过程仍有争议。目前无证明细节与独立验证。

查看原文 ↗

带光滑强迫项的有限时间爆破: Alpöge与Buckmaster在IPM、Boussinesq与Euler方程上的进展

Alpöge与Buckmaster延续Córdoba和Martínez-Zoroa的工作,推进三维不可压缩Navier-Stokes方程的整体正则性难题。目前普遍预期可构造光滑初始数据与光滑强迫项使方程有限时间产生奇点,甚至可能无需强迫项;作者尚未完全实现,但突破使近期完成目标看来可行。他们已在三个更简单模型方程证明有限时间爆破:不可压缩多孔介质(IPM)方程、二维Boussinesq方程和三维不可压缩Euler方程。IPM此前已由Córdoba与Martínez-Zoroa处理,Alpöge与Buckmaster找到可扩展至另两方程并很可能适用于Navier-Stokes的变体方法。工作已在Lean中形式化,论证高度依赖AI辅助;作者正把证明从他们自称“我们见过的数学史上最糟糕的写稿”改写得更专业可读。因外部事件,他们被迫提前发布尚未完全消化和打磨的预印本。Boussinesq论文至少引言质量尚可。

查看原文 ↗

浅层神经网络对混合 Sobolev 空间的逼近

这篇新发布的 arXiv 预印本研究具有混合光滑度 α 的目标函数在 L2 意义下由含 n 个神经元、采用一般激活函数的浅层神经网络进行最佳逼近。作者建立了与激活函数无关的 Fourier-block 原理:若激活函数的一元逼近阶为 ρ,则全局逼近的代数阶为 min{α,ρ},并带有明确的对数因子。对 ReLU^k,匹配的代数下界表明,在任意维度中最优代数逼近指数为 min{α,k+1};该框架也给出 cardinal B-splines 和 soft-ReLU^k 的同一指数,以及 ELU 和余弦激活函数的完整混合光滑度指数 α,均差至对数因子。

查看原文 ↗

AI数学的又一次重要胜利: Claude用11天形式化费马大定理

社交媒体帖文称,Claude 用 11 天完成了费马大定理的形式化,并称这是 AI 在数学上的又一次重要胜利。帖文推测,AI 现在或许终于能够自动化完成将人类高等数学转化为软件可逐行检查的证明这一极其费力的工作;帖文未给出方法、验证程序、论文或数据集等进一步技术细节。

查看原文 ↗

Claude 完成费马大定理首个形式化证明

一项重大数学证明的验证可能需要数年时间。形式化——把数学推理转换为Lean等计算机证明助手可以验证的形式——可以提供帮助。据一则简短社交媒体帖子上月消息,Claude完成了费马大定理的首个形式化证明。帖子未说明该证明的完整内容、发表渠道或评审情况,也未给出更多背景。

查看原文 ↗

Claude 用 Lean 在 11 天内形式化费马大定理并完成计算机验证证明

Anthropic 表示,他们分享了费马大定理的首个完整计算机验证证明。Claude 在 11 天内基本自主地用 Lean 编程语言写出证明,期间生成 1300 万行 Lean,并证明 29,500 个中间定理。费马约在 1637 年提出:对任意 n > 2,不存在正整数 a、b、c 满足 aⁿ + bⁿ = cⁿ。Andrew Wiles 爵士 1995 年的首个证明长达 129 页。此后,包括伦敦帝国理工学院 Kevin Buzzard 于 2024 年发起的多年社区努力,推动用 Lean 证明助手完成形式化。Anthropic 研究员 Tianyi Peng 所在的哥伦比亚大学团队构建 AI 形式化工具;他测试 Claude 能否推进 FLT 形式化,结果超出预期。Buzzard 称,这项自动形式化成就证明 FLT 时除数学公理外没有其他假设,并显示 AI 自动形式化产物已足够稳健、可被继续构建。

查看原文 ↗

AutoGraphForge: 迈向自动化图论发现

AutoGraphForge是一个在建流水线,用于自动提出、反驳、形式化并证明图论猜想。Graffiti3生成器以反例引导方式在初始几百个图、仅随反例增长的快照表上逐轮提出猜想;由559条经典与民间关系构成的新颖性过滤器用线性规划判断是否已被已知结果蕴含,幸存者再在约348,000个图(含House of Graphs不变量导出、至多9个顶点的连通图穷举、若干极值族与随机模型)上测试。在HPC集群上运行数轮后,6,522个猜想通过数据集、新颖性过滤与主动搜索;其中有二部图与正则图的消没数与边覆盖数间的非平凡关系,已手工证明。后续将每个幸存猜想翻译为Lean 4语句骨架;候选证明经固定mathlib4与自定义不变量前导做内核验证,并整合DeepSeek-Prover-V2-671B与OProver-32B两个神经证明器。流水线已通过初步检查,正在运行。

查看原文 ↗

网络比较的最优传输: 综述与机器学习应用

这篇综述探讨如何用最优传输比较无向、无权图,重点介绍三种距离:Wasserstein、Gromov-Wasserstein 和 Bures-Wasserstein。作者考察了一维 Wasserstein 距离通过节点特征概率分布得到的闭式解,并展示 Wasserstein 与 Gromov-Wasserstein 的传输计划如何在图扰动后识别影响距离的具体节点。针对 Bures-Wasserstein 距离,他们利用拉普拉斯谱推导出界,以避免完整谱分解。最后,在合成网络数据集上进行聚类评估,并在真实世界时间序列网络上进行异常检测评估。

查看原文 ↗

基于固定应力分裂与能量自然梯度下降的Biot模型物理信息神经网络

物理信息神经网络(PINNs)作为一种无网格框架近期受到广泛关注,但在求解强耦合多物理场系统(如Biot固结模型)时,因优化地形严重病态而性能下降。本文提出基于PINN的求解器FS-ENGD-PINN,结合物理解耦与几何感知优化:采用固定应力(FS)分裂将多孔弹性系统分解为收缩性力学与流动子问题,以提升训练稳定性与收敛性;采用能量自然梯度下降(ENGD)逼近函数空间中的牛顿方向,缓解刚度引起的缓慢收敛;并引入含总压力的三场混合格式,处理近不可压缩条件下的体积锁定。大量数值实验表明,FS-ENGD-PINN在准确性与鲁棒性上持续优于标准PINN,为宽范围材料参数下的多孔弹性问题提供统一可靠的学习求解器。

查看原文 ↗

基于回归李雅普诺夫函数的稳定性分析与数据驱动验证

李雅普诺夫直接法依赖寻找李雅普诺夫函数。作者把前向不变性放宽为回归性:每条从该集合出发的轨迹都应在有限时间内返回该集合,据此提出回归李雅普诺夫函数(RLF),其子水平集只需满足回归性。温和条件下RLF保证稳定性,更强版本给出渐近与指数稳定性,并配有基于范数的逆定理。作者还提出GPU算法,仅凭轨迹数据即可验证实用稳定性,无需李雅普诺夫函数;验证到ε邻域内只需O(log(1/ε))次轨迹求值,常数随被认证的衰减率接近真实值而增大。

查看原文 ↗

Physics-Informed Stochastic Configuration Machine: 用于非线性微分方程快速训练的无反向传播神经网络

物理信息神经网络依赖反向传播与自动微分,存在计算瓶颈和严重非凸优化问题。研究者提出无反向传播框架 PI-SCM(Physics-Informed Stochastic Configuration Machine):通过解析非线性微分算子的局部雅可比矩阵,将物理损失线性化并投影到统一代数子空间,再由一系列广义线性最小二乘求解器显式确定最优网络权重。该框架包含 PI-SC-I 局部构建、PI-SC-II 滑窗更新、PI-SC-III 全局更新,并证明了普适逼近性质。实验显示,相较标准 PINN,训练过程可加速多个数量级,同时保持高保真预测精度和稳健参数识别。

查看原文 ↗

物理信息误差场学习: 一种物理信息神经网络的训练后优化框架

物理信息神经网络(PINNs)求解偏微分方程时,优化后期继续更新参数往往只带来有限的精度提升,却增加计算开销。为此,论文提出PIEFL框架:在主网络达到满意精度后引入辅助误差网络,将学习目标从解场切换为误差场;在物理约束下推导误差控制方程,使误差网络学习当前近似与精确解之间的偏差,并将所学误差修正与主网络预测结合。该框架无需改动主网络结构,可与现有PINN模型兼容,作为通用训练后优化策略。在代表性偏微分方程上的数值实验表明,它在相同计算预算下能获得更高精度。

查看原文 ↗

用几何不变稀疏自编码器发现大语言模型中的跨语言推理不变性

一项研究通过多语言数学问题(MGSM)数据集,在多个模型的六个语言(英、德、法、西、俄、中)中探究跨语言推理是否依赖共享特征。研究者使用CKA识别对齐层,并训练两种稀疏自编码器:基线模型和新提出的几何不变SAE(GI-SAE),后者通过InfoNCE损失促使编码器对同一问题的不同语言产生相似激活。通过交换特征值并测量KL散度,发现GI-SAE虽提高了几何相似性,但功能可互换性并非一致增强,跨语言共享特征因模型和架构而异,且出现在不同深度。

查看原文 ↗

On-Policy Self-Distillation 中推理路径坍缩的三项调控杠杆综述

On-policy distillation 让教师模型逐 token 评估语言模型自身生成结果,结合模仿学习的稠密监督与强化学习的在策略采样。On-Policy Self-Distillation(OPSD)则由同一模型在参考解、计划或环境反馈等特权信息条件下充当教师;教师并非更强,只是信息更充分。早期结果显示,其准确率可与强化学习相当,且生成 token 数显著更少。但这种信息不对称也会带来偏差,表现为推理路径集合逐渐收窄的坍缩。本文聚焦数学推理,不报告新实验,提出以 token 权重、特权信息性质及教师动态与指导衰减三项杠杆分析坍缩,并区分已定论与仍有争议的问题。

查看原文 ↗

AI验证的几何: iid best-of-N搜索的精确认证极限

验证是目标相对的:证据只能在产生它的干预所解决的方向上认证部署。本文将验证与部署规则表示为可靠性曲面上的核,其跨度几何区分复制(降低抽样噪声)与新干预方向(降低结构盲区)。对iid best-of-N搜索,在标量排序、随机化平局、最大选择、有界二元真值和稳定排序-真值关系下,已知n≤m的best-of-n可靠性后,精确模糊宽度为B_{m,N}=1+2∑_{r=1}^{m}(-1)^r cos^{2N}(rπ/[2(m+1)])。m与√N成正比时模糊约0.83,宽度ε需m~√(N log(1/ε))。由此得到两阶段审计规则:先建立结构覆盖,再加独立任务提升精度;在数学推理和代码选择的回顾性研究中,在82个发现任务上固定的分数尾部审计规则显著降低留出误差。几何仅适用于已知或独立估计的核;经验分析仅为说明性,而非前瞻性干预。

查看原文 ↗

生成神经网络用于Sinkhorn分布鲁棒假设检验

本文研究Sinkhorn分布鲁棒假设检验问题,针对以经验分布为中心的Sinkhorn差异模糊集,提出一种生成式框架以学习最不利分布。作者推导了该模糊集与核平滑参考分布的条件KL散度的等价表示,并证明约束与非约束极小极大SDRHT公式的强对偶性。利用闭式最优检测器和Brenier定理,将最大最小对偶问题重述为对凸势函数的最大化,其梯度刻画可逆传输映射。采用Hyper输入凸神经网络(HyCNNs)及随机梯度估计器近似这些势函数,并证明其表示能力和诱导传输映射的分布普适性。数值结果表明,该方法在不同样本量和维度下具有优越的准确性和鲁棒性,且避免经典SDRHT方法可扩展性的局限。

查看原文 ↗

高等线性代数及其应用——第一部分(偏微分方程、机器学习和数据同化中的数值线性代数)

本讲义是数值线性代数高级硕士课程的第一部分,旨在展示该学科比上一代更为核心的原因。数值线性代数伴随偏微分方程的数值求解发展,但如今网络节点排序、天气预报中的数据同化以及大型噪声数据的模型拟合,都产生无法直接分解、结构特殊且只能通过矩阵-向量积访问的问题。讲义涵盖范数、分解、条件数和浮点运算;来自有限差分、图和机器学习的稀疏矩阵;平稳迭代与光滑性;共轭梯度与Lanczos方法,包括谱聚类和早停正则化;Arnoldi与GMRES,用于PageRank和大型最小二乘;最后是预条件、Schwarz区域分解和多重网格。假设读者已修过线性代数基础课程,每节附有要点总结,每章配有练习(含历年考题),并附Python代码复现数值示例。

查看原文 ↗

菲尔兹奖得主将加入 OpenAI, 约 40 位数学家齐聚 AI 与数学未来闭门峰会

上个月刚获菲尔兹奖的 Jacob Tsimerman 宣布将加入 OpenAI 从事 AI 安全研究。8 月初,他与研究科学家 Sébastien Bubeck 在旧金山总部召集约 40 位数学家闭门开会,一场报告题为《The End of Mathematics》。多伦多大学教授 Daniel Litt 警告人类数学专长可能完全消失,但认为极端情形可能性不大;MIT 的 Drew Sutherland 称数学家或许是“煤矿里的金丝雀”。数学被视为高级认知能力的代理指标。5 月,未发布的 OpenAI 模型用代数数论工具推翻单位距离猜想;8 月,OpenAI 宣布 10 项新发现;Anthropic 的 Levent Alpöge 用 Claude 在 668 维超立方体上构造出正交向量对。

查看原文 ↗

欢迎来到数学领域的人工智能危机

在本期Decoder节目中,The Verge驻伦敦的AI记者Robert Hart讨论了AI对数学领域的冲击,以及许多顶尖数学家因此面临的生存危机。OpenAI刚发布的一系列数学难题解决方案在数学界引起轩然大波,引发激烈辩论。尽管AI在小学算术上仍表现不佳,但在高端抽象数学上却日益擅长,这提出了重大问题:若AI能胜任高水平数学,其能力能否迁移至其他领域?学术拨款和大学培养新数学家的意义何在?又或者,这一切只是前沿AI实验室的市场营销手段?Robert访谈了多位知名数学家,探讨这些议题。

查看原文 ↗

粗粒化多尺度偏微分方程动力学的通量形式时空神经算子

该研究关注多尺度PDE系统的粗粒化动力学数据驱动预测。采用无闭包的算子学习视角,应用线性粗粒化映射,直接从滤波高保真轨迹学习分辨场的替代演化算子。受Mori-Zwanzig形式启发,提出时空神经算子,将分辨历史板映射到未来板。空间混合使用傅里叶卷积,时间混合使用因果核算子。通量形式的归纳偏置提高滚动稳定性。在粘性Burgers方程、Kuramoto-Sivashinsky方程和二维湍流中验证,获得稳定自回归滚动和改进的长时精度。

查看原文 ↗

关于Rashomon集、简单性的数学, 以及为什么我们不需要黑箱: Cynthia Rudin访谈

本期AI先驱访谈节目对话可解释机器学习先驱Cynthia Rudin。她因开发可解释算法而获2022年松鼠AI奖,其算法已用于癫痫预测、犯罪检测和生物研究。Rudin分享了与Con Edison合作维护纽约电网的早期经历:黑箱方法失败后,简单模型的准确性反超黑箱。她指出,在高风险问题中,数据噪声大,黑箱并不一定更准确。她致力于用数学证明简单模型的有效性,并探讨了Rashomon集等概念。

查看原文 ↗

Hyra 数学更新: 3D 常数宽度体的下界提升

Hyra 继续推进数学前沿。自上次数学更新以来,又取得了四项进展:3D Blaschke–Lebesgue 问题将常数宽度体的通用下界从 0.380799w³ 提高到 0.411040w³,现在已达到猜想中 Meissner 最优值的 97.9%。此外,还有 Beurling–Ahlfors 等其他进展。

查看原文 ↗

Palomar——Lean 验证数学注册中心

陶哲轩近日宣布,Palomar——一个由 Lean FRO 和 ICARM 孵化的 Lean 验证数学注册中心现已开放提交。该中心旨在作为 Lean 证明的预印本服务器,接受包含挑战文件、解决方案模块和 formalization.yaml 的 GitHub 仓库快照。提交后,系统将检查解决方案模块是否类型检查并通过挑战文件中的声明,以及非正式描述是否与正式声明匹配。陶哲轩担任科学顾问委员会成员。这一举措旨在应对 AI 生成的 Lean 证明日益增多但验证困难的问题。

查看原文 ↗

经验链: 大型语言模型的持续改进

本研究提出“经验链”(Chain-of-Experience, CoE)范式,让大型语言模型(LLM)在测试时通过与自我或环境反馈的迭代交互积累经验,实现持续改进。在数学、编程和知识领域,使用8种LLM(包括GPT-5、Gemini-2.5 Pro、Claude-4.5 Sonnet)评估,发现利用迭代经验一致优于无反馈基线,仅自我反馈即带来显著提升,总体提升5.6%,API成本降低19%。结合互补反馈通道(如模型与正确性信号)可进一步增益,且CoE在每token准确率上优于现有测试时策略。模型基础能力与改进能力正相关,且在弱或虚假反馈下仍保持稳健。

查看原文 ↗

大型语言模型中浮现模块化认知架构

人类大脑具有显著的功能专门化:不同网络分别支持语言、形式推理、对他人心理的推理和对物理世界的推理。本文考察大型语言模型(LLM)——经由非常不同的优化过程产生的另一类智能系统——是否也会出现类似组织。基于覆盖语言、形式推理、社会推理、物理推理四个认知领域的N=46项任务的电路分析,研究发现LLM会形成与人类大脑镜像的模块化架构:人类中由同一网络支持的任务在LLM中招募重叠的神经元,由不同网络支持的任务则招募不同的神经元。这种模块性在脑与神经网络中的趋同出现提示,它可能是智能系统的基本属性。

查看原文 ↗

版本更新下没有通用信号能预测样本级LLM回退

前沿LLM更新后通常在整体上优于旧版,但整体提升不能说明单个样本:更新仍可造成样本级回退,即旧模型正确而新模型错误。本文用统一的增量价值检验,将各信号相对于置信度基线的增益分离出来,比较推理时可得的单模型信号(置信度、logit间隔、注意力熵)与跨版本信号(输出KL散度、似然漂移、token级KL、表示漂移)。在六个基准、三个任务族(多项选择问答、数学推理、代码生成)和六组模型更新对上,信号有效性依赖任务;没有信号普遍最优;部分跨版本信号在置信度失效时仍有信息量,包括无标签情形,并支持将高风险样本退回旧模型的概念验证。代码见项目仓库。

查看原文 ↗

基于扩散模型的离线深度Q*估计

在离线强化学习中,基于离线观测数据估计最优动作价值函数Q*可通过求解最优贝尔曼方程实现。但奖励函数和转移核未知,最优贝尔曼算子无法直接观测。本文提出将算子估计与价值函数学习解耦的框架:先用条件扩散模型估计奖励规律和转移核,构建数据驱动的最优贝尔曼算子近似,再通过最小化经验贝尔曼残差获得Q*的深度估计。理论上,文章建立了学习最优贝尔曼算子的尖锐非渐近收敛率,并给出残差风险和L2收敛率的上界,且无需深度RL理论中常用的完备性假设。大量数值实验验证了方法的有效性。

查看原文 ↗

问题本身即问题: 迈向可扩展的数学发现

AI系统日益能贡献数学研究,但前沿模型推理和专家评审都是稀缺资源,需合理分配。现有AI数学工作流中,人类精力集中在选题和评审两端,成为瓶颈。为此,研究者提出新的人机协同发现范式,人类提供研究方向,系统在文献中搜索候选问题。他们构建了名为FAR(Find, Attempt, Recommend)的流水线,从5245篇组合学论文中恢复6453个候选猜想或开放问题,筛选出4717个表述良好且仍未解决的问题,经推理和自动筛选后,选出598个潜在解法,最终77项进入作者团队评审,其中包含对Davies–Jenssen–Perkins–Roberts、Erdős–Straus、Ikenmeyer–Pak–Panova及Lund–Saraf–Wolf等猜想和问题的发现,展示了这种新协作模式的有效性。

查看原文 ↗

MathCode: 为终端编码智能体引入 Lean 4 形式化引擎

这是一个开放工具与工作流原型,不代表自主定理证明已经解决。项目页把 MathCode 标为 2026 年 4 月项目,当前列出的最新版本 v0.2.0 发布于 5 月 26 日;这里列在 8 月 16 日,是因为 Hacker News 讨论让它重新进入公共视野。最值得关注的是围绕 Lean 形成紧密的“编写—编译—诊断”闭环;已核验的项目页面没有给出证明成功率、基准对比,仓库也未显示明确许可证。

查看原文 ↗

MathForm: 通过知识检索与验证引导的精炼实现数学自动形式化的规模化

自动形式化通常被视为将自然语言数学命题翻译为机器可验证的正式语言(如 Lean 4)。然而,忠实的形式化需要将数学概念映射到 Mathlib 等正式库中的类型和定义,现有方法依赖参数记忆而缺乏反馈修订。本文提出 MathForm 框架,通过 Mathlib 知识检索和验证引导的迭代精炼构建经校验的训练数据。利用该框架构建了 FormalVerse 数据集,包含约367K个 Lean 4 验证示例,并训练了 MathForm-8B 模型。在六个基准测试中,MathForm-8B 在语法检查和一致性检查下的平均 Pass@8 分别为 88.06% 和 72.37%,优于多个专业的 32B 自动形式化系统;在 FATE-H 和 FATE-X 子集上,CC 通过率分别为 63% 和 37%,均超过最强基线。

查看原文 ↗

Google DeepMind 的 Pushmeet Kohli 谈 AlphaEvolve 与 AI 科学发现

谷歌 DeepMind 研究副总裁 Pushmeet Kohli 主管 AI for Science,介绍团队开发的 AlphaEvolve:将大语言模型与进化搜索结合,可发现全新算法、证明困扰研究者数十年的数学结果,并改进了已有 50 年历史的矩阵乘法算法,还能为数据中心调度等问题生成可解释代码,合作对象包括数学家陶哲轩。Kohli 提出「harness」架构,强调强大生成模型须配以可靠的领域评估器,才能区分幻觉与洞见。AlphaEvolve 的突破来自去掉人为提供的模板、搜索完整算法而非代码片段。多智能体系统让模型互相批评、改进与排序,DeepMind 的 AI co-scientist 经数天计算显著提升;模型往往更擅长评估想法而非生成想法,因此宜分离生成者、批评者与编辑角色。

查看原文 ↗

对Sendov猜想证明的消化: AI生成证明经Lean验证后整理并完全解决相关猜想

帖子讨论Sendov猜想、其Phelps–Rodriguez加强版以及内点版本Conjecture 3。此前这些猜想在部分情形和充分大情形已有结果,中间情形未决。最近Lech Mazur用AI工具解决Sendov猜想,证明经Lean验证,但AI生成的证明尚未整理成可发表预印本。作者花数日、借助大量AI辅助进行消化,将其置于既有文献语境并简化以突出核心思路;聊天记录仅占整理工作的一部分,其余用纸笔或更多AI代理完成。相同论证还给出Rubinstein定理的新证明,并表明Conjecture 3成立,从而完全解决Sendov猜想与Phelps–Rodriguez猜想;证明相当初等,未使用复分析。

查看原文 ↗

MindTopo 揭示了多模态模型的空间推理能力

MindTopo 是一个新基准,用于测试多模态大语言模型的拓扑推理能力,评估其对连通性、封闭性、顺序、分离和打结等概念的理解。该基准既测量静态图像中的识别能力,也测量通过一系列动作保持和操作这些关系的能力。研究发现,当前模型在静态识别上表现较好,但在交互任务中表现不佳,表明它们在时间上维持一致拓扑理解方面存在困难。失败通常发生在规划阶段而非感知阶段,模型在场景变化时会丢失结构关系或提出违反物理约束的动作。这些发现强调了推进 AI 系统在机器人技术和交互环境中发展的机会。

查看原文 ↗

LLM擅长什么样的数学?

Gowers 并未把现象简单归结为模型偏爱存在性命题。他更关心求解过程:模型可以跨领域调用知识,并行尝试大量人类不会投入的低概率路径;短板则可能是数学家的“鼻子”——能否尽早判断哪条路值得走、迅速剪掉无望分支。他给出的更高验收标准是:AI 不只做出答案,还提出真正新颖、出人意料、事后看来又自然,并能被其他数学家继续复用的方法。

查看原文 ↗

进一步了解 Claude 的数学能力

Anthropic 的一名员工给未发布的研究版 Claude 布置了一个近乎不可能的挑战:认真尝试黎曼猜想。Claude 并未成功,但在过程中意外改进了黎曼ζ函数满足黎曼猜想的零点占比的已知下界,将这一长期由数学家逐步推进的比例从 41.6% 提高到 67.2%。供职于 Anthropic 的两位数学家审阅并验证了 Claude 的论文,为专家撰写了简洁的非正式说明;Claude 还生成了可形式化验证的证明。外部专家 Brian Conrey 和 Dan Goldston 在短时间内审阅了该论文。Anthropic 不认为这些技术会导向黎曼猜想的证明,但称这是 AI 模型数学能力快速进步的最新例证。

查看原文 ↗

HRT反例的部分消化

陶哲轩讨论了Heil-Ramanathan-Topiwala(HRT)猜想,该猜想断言具有合理衰减条件的非零函数不能由不同的时频位移线性组合为零。文章指出,当位移均为频移或共线时,猜想成立;对于晶格情形,可利用交换性通过对函数在陪集上的限制将关系转化为逐点方程。作者称该结果部分回应了HRT反例,但未提供反例具体构造。

查看原文 ↗

OpenAI宣布下一个前沿模型Astra: 内部版本攻克10个长期开放难题

美国AI公司OpenAI宣布其下一个主要模型家族Astra。公司称,由“一个内部版本的Astra”取得了10项成果,每项都解决或大幅推进了一个长期开放问题,领域涵盖高维几何、编码理论、算术线路复杂性、群论、算子代数、量子复杂性、格密码学与极值组合学。具体问题包括高维球堆积、二元码与球面码、非sofic群、Connes刚性猜想、量子并行重复、最近向量问题、Ehrhart体积猜想、多色Ramsey数与极值数猜想等;其中模型给出了某些群由其von Neumann代数唯一决定这一长期猜想的反证,并给出降至Cohn–Elkies阈值的球堆积密度新上界。据The Telegraph报道,OpenAI首席执行官Sam Altman上周访问华盛顿时被认为向美国政客演示了Astra系统。OpenAI研究科学家Noam Brown在LinkedIn发文称,该内部版本在数学、量子复杂性与理论计算机科学中解决了10个重大开放问题。哥伦比亚大学副教授He

查看原文 ↗

OpenAI: Astra内部版本在10个数学与理论计算机科学长期难题上给出新结果

OpenAI称其下一代模型Astra的内部版本在数学与理论计算机科学的10个长期悬而未决的问题上产出新结果,这些问题的主要结果至少十年未见进展,许多停滞更久。研究覆盖高维几何、编码理论、群论、算子代数、量子复杂度、格密码学与极值组合学,成果包括:达到Cohn-Elkies阈值的高维球堆积新上界、给定最小距离下二元码最大尺寸的改进界、非sofic群存在性的构造、对Connes刚性猜想的证伪、n⁴/log n量级的算术公式下界、一般双人量子博弈的指数并行重复定理,以及最近向量问题的多项式因子近似困难性结果;另有Ehrhart体积猜想与多色Ramsey数等工作。

查看原文 ↗

陶哲轩在ICM演讲警示: AI或产出超出人类处理能力的数学证明

菲尔兹奖得主陶哲轩在国际数学家大会(ICM)发表演讲《Mathematics in the Age of AI》,把当下比作1900至1930年的动荡期:罗素悖论(1901)与哥德尔不完备定理(1931)曾迫使数学家重审学科基本假设,而他认为数学正进入“数学价值与实践基础的危机”。他援引5月的First Proof实验——受控条件下前沿AI模型解出10道研究级新问题中的7道,证明经专家审阅、具发表水准——并据此提出“工作假说”:AI工具“相当快”即可完成相当比例的研究级数学任务,成功率、质量、监督与成本均合理。若假说成立,核心问题将从AI能做什么,转向数学共同体的目标与价值何在。

查看原文 ↗

关于《莱顿宣言》的思考

作者参加了一场关于数学与AI的研讨会,会上产出了《莱顿宣言》,已有3000多人签署。作者虽未签署,但并非反对,而是对宣言中一些自信的断言和建议感到不确定。他强调宣言在聚焦数学界面临AI问题上的积极作用,并引用了宣言中关于数学研究特征性价值的段落,包括证明的最高确定性、归因性、透明性和独立验证性等。

查看原文 ↗

我们如何刻画智能体网络中的共识达成?

信念流网络(Belief Flow Networks)研究有向影响力图上智能体间的信念交换。每个智能体持有复杂逻辑信念(如条件性陈述),并通过异步更新进行信念修正,且不同智能体可采用不同理性变更策略。该研究探讨若影响力能够从每个智能体传播至其他所有智能体,群体是否终将达成共识,以及共识的具体内容。这与数值平均不同,需考量信念修正的复杂逻辑。文章回顾了信念修正及改进算子等相关领域。

查看原文 ↗

雅可比猜想反例的消化

陶哲轩在博文中讨论了雅可比猜想,即复多项式映射局部可逆(雅可比行列式非零常数)则整体可逆。最近利用Fable AI在三维中构造了反例,给出显式七次多项式,其雅可比行列式为非零常数但映射不可逆。尽管验证简单,但构造看似奇迹,涉及大量抵消。该反例随后被几何解释,陶哲轩试图以较少代数几何知识进行消化。二维情形仍开放。

查看原文 ↗

人类数学家正被反例超越

在形式化与AI工具的交汇处,反例成为焦点。2026年5月20日,ChatGPT反驳了离散几何中的Erdős单位距离猜想,人类数学家虽经核查但未在Lean中形式化。五天后,Logical Intelligence(由Turing奖得主Yann LeCun共同创立)将其自动形式化于Lean中。该证明依赖Golod-Shafarevich定理,该定理的证明需100多页且涉及全局类域论,目前全局情形尚未形式化。Buzzard的学生Edison Xie正在完成局部情形的PhD项目。

查看原文 ↗

可视化Gilbreath期望序列

陶哲轩在博客中展示了如何利用编码代理将论文中的图转化为交互式动画。他以最近与Chase和Hunter合著的关于Gilbreath猜想的论文中的图1为例,该图绘制了“Gilbreath期望序列”的精确值和数值模拟值。该序列由倒金字塔状的Gilbreath数组定义,顶部为指数随机变量,其余为相邻差的绝对值。序列为左侧对角线的期望,论文中仅计算了部分理论值,其余通过蒙特卡洛模拟获得。Michael Ross扩展了理论值,与模拟吻合良好。序列的渐近行为仍未知,甚至无法证明有界,论文中仅证明了其衰减不会快于某个界限。

查看原文 ↗

论文图表可视化工具

陶哲轩开发了一款应用,可将论文中定理对象之间的依赖关系(以JSON格式输入)转化为交互式图表,支持探索、编辑并导出为SVG、TikZ、quiver或Mermaid等格式。他利用LLM为八篇论文生成了示例图表,包括Wang和Zahl对三维Kakeya猜想的证明、Wiles对费马大定理的证明以及Szemeredi定理的证明等。陶哲轩指出,当前瓶颈在于审查过程而非代码生成,并希望用户能自行创建或借助AI工具生成图表。

查看原文 ↗

旧应用与新应用, 借助现代编码代理

陶哲轩自1999年起编写Java小程序用于数学教学与可视化,后因浏览器不再支持Java而失效。近日,他利用AI编码代理将这些旧小程序移植到JavaScript,并添加了图形改进,如将Besicovitch集应用彩色化。移植约二十多个应用仅发现一个次要bug,且代理还指出了原代码中的两个错误。受此鼓舞,他重启了1999年放弃的特殊相对论可视化工具构想,类似“闵可夫斯基空间中的Inkscape”。

查看原文 ↗

采访Thi Kieu Khanh Ho: 时间序列异常检测

在AAAI/SIGAI博士联盟系列访谈中,麦吉尔大学和Mila-魁北克AI研究所的博士生Thi Kieu Khanh Ho介绍了她的研究。她专注于时间序列异常检测,旨在在标记数据稀缺、嘈杂或受污染的情况下,教会AI系统识别真实世界数据流中的异常。她的方法可应用于医疗、工业监控和预测性维护。她开发了EEG-CGS,一种无需标记癫痫样本即可检测脑电图(EEG)异常通道的自监督框架;以及TSAD-C,一种处理训练数据本身含有异常情况的多元时间序列异常检测框架。她还撰写了关于自监督学习和基于图的时间序列异常检测的综述。

查看原文 ↗

《Marcus on AI》审视 OpenAI 在 Erdős 问题上的成果

「Marcus on AI」对 OpenAI 在 Erdős 问题上的成果提出质疑。文中转述 Cal Newport 的邮件:OpenAI 用一款尚未发布的推理模型,通过 chain-of-thought 式「出声思考」,帮助找到一个反例,推翻了 Paul Erdős 80 年前提出的离散几何猜想;职业数学家从长篇推理记录中识别反例并改写为标准证明。审阅完整输出的数学家 Thomas Bloom 指出,研究者多认同 Erdős「猜想为真」的信念而专注求证,大模型工具却系统运用并扩展已有技术、寻找猜想为假的证据;AI 常沿人类认为不值得尝试的路径坚持,兼具超人耐心与广泛技术储备。作者另指出,近年 LLM 已与计算机辅助数学工具结合,系统探索人力难以持久钻研的问题空间。

查看原文 ↗

“Formalizing Fermat”工作坊

“Formalizing Fermat”工作坊将于2026年7月6日至10日在伦敦举行,目标是推进EPSRC资助的、在Lean中形式化费马大定理的项目。组织者称,项目最初设想是把FLT化归到1980年代已知定理,即形式化Wiles/Taylor–Wiles论文;实际路线则是更现代、思路可追溯至Khare策略的证明。组织者刚完成11讲相关课程,并将与数论/Lean专家及自动形式化专家合作,试验AI能否形式化所需前提乃至核心证明思想。他认为自动形式化虽有进步,但尚不能可靠地自主形式化定义或定理陈述;定义密集的复杂部分可能效果差,而mathlib中定义齐备、人类文献记录充分的部分可能效果好。

查看原文 ↗

最近使用 ChatGPT 5.5 Pro 的一次体验

作者(蒂莫西·高尔斯)称,由于使用 ChatGPT 5.5 Pro,他大幅上调了对大语言模型数学能力的评估。该模型在大约一小时内产出了一篇博士水平的研究成果,且作者未提供严重数学输入。他提到,LLM 已能解决研究级问题,包括一些 Erdős 问题,但初期许多“解法”不过是检索文献中已有答案。然而,笑声渐弱:LLM 已能发现人类数学家因种种原因遗漏的简单论证,尽管这些论证往往有先例。作者计划探索组合学中新参数引发的未解问题,测试 LLM 是否仍能解决。

查看原文 ↗

陶哲轩等UCLA团队获Laude Moonshots种子资助, 开发数学研究AI伙伴

由计算机科学教授Amit Sahai领衔、数学教授陶哲轩参与的UCLA六人跨学科团队,获得Laude Institute提供的25万美元种子基金,属于该机构首届Moonshots计划。团队从美国与加拿大47家机构、600多名研究者提交的125份提案中脱颖而出,是仅有的8个入选项目之一。项目名为“Accelerating the Queen of Sciences”,目标是开发能进行严格且创造性数学思考的AI系统,最终成为各定量领域科学家的研究伙伴。团队不训练AI求解已知问题,而是教它像数学家一样行事,并让论断得到自动验证,把“听起来对”变成“确实对”。Sahai表示,最令他期待的是让AI具备在数学中做出惊奇驱动之发现的能力。

查看原文 ↗

AI时代中的数学方法与人类思维

本文由Tanya Klowden和陶哲轩联合撰写,探讨人工智能与形式化如何改变数学的目的、实践及社会角色。文章指出,AI和数学形式化可能重塑数学研究的本质,影响数学家的日常工作方式以及数学在科学和社会中的应用。作者强调,尽管AI工具日益强大,但人类的数学直觉和创造性思维仍不可或缺,技术变革将重塑人与数学的关系。

查看原文 ↗

《AI已“碾压”人类考题》: 陶哲轩与Mark Chen对话——大语言模型不再是“数学差生”

在IPAM研讨会上,菲尔兹奖得主陶哲轩与OpenAI首席研究员Mark Chen进行炉边对话,讨论AI在数学领域的飞跃。一年前陶哲轩评价GPT像“效率极低的博士生”,如今AI已在IMO获金牌级成绩,人类编写的基准测试被迅速“击破”。陶哲轩认为数学试错成本低,AI快速解决长期被忽视的Erdős问题,促使数学界反思研究分工、人机协作与教育变革。

查看原文 ↗

陶哲轩谈生成式AI的数学前景: Erdős问题解答只是“廉价的胜利”

围绕AI撰写证明的讨论,很大一部分热度来自这些证明的裁决者陶哲轩。据The Atlantic报道,这位加州大学洛杉矶分校教授被广泛视为当今在世最伟大的数学家。但陶哲轩在接受采访时,对AI能为数学带来什么态度更为克制。他说,AI生成的Erdős问题解答确实令人印象深刻,却算不上震撼;这些机器人在功能上取得了一些“廉价的胜利”。

查看原文 ↗

Gemini Deep Think: 重新定义科学研究的未来

Google DeepMind 称,Gemini Deep Think 在专家数学家和科学家指导下解决数学、物理和计算机科学中的专业研究问题。2025年夏,一个高级版本在国际数学奥林匹克(IMO)达到金牌标准,更新版本随后在国际大学生程序设计竞赛(ICPC)取得类似成绩;团队最近一周发表了两篇相关论文。研究级数学方面,团队构建了基于 Gemini Deep Think 的智能体 Aletheia,用自然语言验证器发现候选解法缺陷并迭代修正,且能承认失败;为应对高级科目中因数据稀缺造成的浅层理解与幻觉,它还使用 Google 搜索和网页浏览,避免虚假引用和计算错误。模型在 IMO-ProofBench Advanced 上随推理时计算扩展得分最高达90%,而 Aletheia 显示更低推理时计算也能实现更高推理质量。

查看原文 ↗

加速数学

本文探讨如何利用科技加速数学发现。传统上,政府通过资助机构和中心支持个人及小团队研究前沿问题。作者认为,尽管大型语言模型(LLM)和交互式定理证明器(ITP)有望颠覆数学研究,但目前尚无“杀手级应用”。专家们使用LLM进行头脑风暴、文献检索和解决中间问题,而业余爱好者则产生大量经不起推敲的“突破性”论文。作者对非专家仅凭这些工具投身研究数学表示怀疑,并对AI生成的低质量内容感到沮丧。

查看原文 ↗

FrontierMath: 开放问题

Epoch AI发布了一个包含14个研究级开放问题的试点项目,这些问题具有可编程验证的答案,旨在测试超越现有基准的前沿能力。

查看原文 ↗

Erdős问题的形式化

本客座文章由Boris Alexeev撰写,介绍围绕Erdős问题的近期进展,特别是利用人工智能对旧新数学进行形式化。背景:保罗·埃尔德什提出了大量猜想,Thomas Bloom于2023年5月建立erdosproblems.com跟踪进展。2025年8月添加论坛,2025年5月Google DeepMind启动形式化猜想项目。Bloom和陶哲轩提议将网站与OEIS链接。目前网站上有1100多个问题,约40%已解决,约240个问题在Lean中形式化,17个有形式化解,260个链接到OEIS。文章还提及人类无AI形式化的早期例子,如Bloom和Mehta形式化单位分数问题。

查看原文 ↗

Google DeepMind与菲尔兹奖得主陶哲轩详述AlphaEvolve的AI数学发现

Google DeepMind与数学家陶哲轩等合作者本周发表论文,介绍AlphaEvolve推动的数学发现。该工作展示了纯数学中人机协作的新方法。该系统处理了67个挑战性问题,既重新发现顶尖解,也为若干长期挑战找到新构造。AlphaEvolve被称为“通用进化编码代理”,借助Gemini等大语言模型提出、测试并迭代改进算法解,建立在DeepMind 2025年5月首次发布该工具的工作之上。陶哲轩在博客中解释,其核心是进化用于寻找解的Python代码,而非直接构造数学对象;“搜索模式”让一次较慢的LLM调用触发大规模廉价计算,并自行探索数百万种可能性,“泛化模式”则寻找对任意给定数成立的公式。研究者称,许多问题的平均准备时间最多只需几小时。源文本在列举具体新方法处截断。

查看原文 ↗

形式化还是非形式化?人工智能证明定理之问

计算机证明数学正处于有趣时期。对于计算机能否自主证明研究级数学定理,作者持不确定态度,但更看好AI成为数学家的有用助手,正如其当前用Lean教授研究级定义和证明的工作。就IMO问题而言,有四种公开尝试:两种用语言模型写英文证明(非形式化),两种用语言模型与Lean混合(形式化)。作者担忧非形式化方法:期刊收到越来越多由LLM生成的看似合理的论文,且有时未披露使用,并列举LLM论文与人类论文的差异,如LLM倾向于迎合。

查看原文 ↗