数学
73 条内容
AI4Math 综述:从引导猜想到形式化证明,AI 已能解出 PKU 研究生考题并在 Lean 中验证 Erdős 问题的反例
这篇综述系统梳理了 AI for Mathematics(AI4Math)的进展、挑战与前景,将研究分为面向特定问题的建模(引导直觉、构造反例、封闭系统形式推理)与通用建模(自然语言推理、形式推理、数学信息检索)两条互补路线,并报告了作者自建的 PKU 本科与博士资格考试评测:GPT-4 平均分低于 60,而 o1、DeepSeek-R1、o3-mini、Gemini 2.5 Pro 等推理增强模型多数超过 90,o3-mini 在 58 道博士资格考试题上平均 84.4 分,同时指出研究级数学仍是开放难题。
Steinwart 用 Banach 空间值鞅方法证明:联合高斯变量的条件分布仍为高斯,且可由有限维滤波序列逼近
该工作研究两个 Banach 空间值联合高斯随机变量的条件分布,证明条件分布仍为高斯测度,并给出一个基于滤波序列的有限维逼近方案:条件均值在 E 范数下收敛、协方差算子在核范数下收敛、条件概率弱收敛,且这些结果在连续高斯过程对路径的部分无穷观测条件下给出均值与协方差函数的一致收敛。
Bhattacharya、Deb 与 Mukherjee 把多线性 Gibbs 测度的自由能极限写成无穷维优化问题,并给出复制对称的充分条件与反例
本文研究哈密顿量为广义 U-统计量、基测度任意的多线性 Gibbs 测度,在耦合矩阵按割范数收敛的条件下,把自由能极限表示为函数空间上的无穷维优化问题,给出复制对称(优化子为常函数)的充分条件并用反例说明其必要性,进而得到局部场、哈密顿量与全局磁化等统计量的弱极限、对比量的普适弱定律 n^{-1}Σc_iX_i→0(当 Σc_i=o(n))、局部与全局磁化的指数集中界,以及高阶相互作用下温度参数的相变点存在性。
杨美佳与夏勇证明:广义迹比问题需同时添加冗余约束并缩放才能消除拉格朗日对偶间隙
本文研究定义在Stiefel流形上、目标为迹形式二次分式的广义迹比问题(GTRP),基于新建立的矩阵S-引理证明:若先添加冗余约束XX^T⪯I_n并做良好缩放得到等价问题(GRS),则其拉格朗日对偶间隙为零;而单独添加冗余约束(GR)或单独缩放(GS)以及原问题(GTRP)本身都可能存在正的拉格朗日对偶间隙。
用 FLAME 方法系统推导斜对称矩阵 LTLT 分解算法,融合 BLAS 类运算后性能较 PFAPACK 与 Pfaffine 大幅提升
该工作用 FLAME 形式化方法系统推导斜对称矩阵 X = LTLT(L 为单位下三角、T 为斜对称三对角)三角三对角化的一族算法,给出无主元与带主元的多种分块右看、左看及融合变体,识别出新的 level-2 与 level-3 BLAS 类运算,并借助 BLIS 2.0 的打包机制与 OpenMP 并行实现,实验表明其最佳实现性能大幅超过此前唯一已知软件 PFAPACK 与 Pfaffine,同时与相关对称矩阵分解软件相当或更优。
Schneider 以 Navier-Stokes 有限时间爆破证明为例,论证 AI 预测只有在可审计的因果链中才能被信任
Tapio Schneider 以 OpenAI 于 9 月 8 日宣布的强制 Navier-Stokes 方程有限时间爆破证明为切入点,区分了作为解释性理解的 episteme 与作为预测技艺的 techne,主张当预测必须在被经验验证之前就被信任时(如数十年气候预估、新构型飞机设计),信任来自从假设与输入数据到结果的、每一环都可单独检验的可审计因果链,因此 AI 应嵌入守恒律等可审计脚手架中,用于学习可被高分辨率模拟、观测或实验检验的闭合模型,而不是采用端到端模型。
ReLU 卷积网络在 Korobov 空间把逼近阶从二阶提升到 m+1 阶,误差随维度的增长远弱于 Sobolev 情形
该工作研究用 ReLU 深度卷积神经网络(CNN)逼近高阶 Korobov 函数 f∈K^{m+1}_p(Ω) 的 Lp 误差,证明当深度 L≤Csd^4m^3N(log_2 N) 时存在网络使 inf‖f−f_L‖_{Lp(Ω)}≤C_{m,d}‖D^{m+1}f‖_{Lp(Ω)}N^{−m−1}(log_2 N)^{(m+2)(d−1)},即把以往基于二阶混合导数的 O(L^{−2+1/p}) 阶逼近率提升到 (m+1) 阶(相差对数因子),并据此指出 CNN 的高阶表达能力并未严重受维度灾难影响。
Scholes 提出:生命或许不靠真正的量子效应,而是用经典振荡网络“数学上模仿”量子行为
化学家 Gregory Scholes 与其合作者在过去三年的一系列论文中提出并演示,由大量相互作用的经典振荡单元组成的复杂网络可以涌现出在数学上等同于希尔伯特空间向量的状态,从而“量子式地”模仿量子比特、叠加与干涉,为量子生物学提供了一条不依赖真实量子相干性的替代解释路径。
Lean Pool:由 AI 代理维护的形式化数学档案库
Lean Pool 是一个由 AI 代理生长、维护与优化的形式化数学仓库,论文报告其截至 2026 年 9 月 21 日已汇集 211 个已完成项目、3,228,485 行 Lean 代码、18 位提交贡献者,并通过代理辅助的依赖升级、证明压缩与数学评审来维持这些独立开发的形式化成果在 Lean/Mathlib 演进中持续可用。
第 5 页 · 当前显示 10 项