全部 AI4Math 动态 先扫描摘要，再展开感兴趣的内容。订阅 AI4Math Radar RSS →
10月23日 ⌄ 星期五 · 11 条
08:00
Patrick Lopatto / Hexagon 精选 AI 评分 97 ☆ Patrick Lopatto 于 10 月 23 日在 Hexagon 首发关于实对称高斯正交系综（GOE）体区相邻特征值最大间隙的论文。作者主张经显式中心化与缩放后，固定体区中的极端间隙收敛到具有指数强度的 Poisson 点过程，最大间隙呈移位 Gumbel 极限；这是对 Feng–Wei 已处理 GUE 情形的不同对称类推广。关键论证以任意有限矩阵规模下 GOE 与 GUE 空隙概率的行列式恒等式为桥梁，并用 Nazarov 不确定性原理、Hermite 函数恒等式处理增长尺度。提交者明确披露 GPT-6 Astra、GPT-6.1 Sol 与 Claude Opus 5.5 参与发现、核查和撰稿，且仅理解部分证明。本条是未经过外部独立同行审稿的 AI-assisted 研究主张，未发现 Lean 端到端证明。
数学发现
推荐理由：将 AI 辅助数学发现推进到随机矩阵极值统计的具体深层结果，同时提供明确的概率极限结论、经典比较对象及模型参与声明；必须区分作者证明主张与第三方确认。
08:00
Haruhisa Enomoto / Hexagon / Palomar 精选 AI 评分 96 ☆ Haruhisa Enomoto 于 10 月 23 日公开表示有限有限维代数的结构论研究：基于 Auslander–Reiten quiver、mesh 关系、radical 分层与 filtered deformation，试图重新证明 Bautista–Gabriel–Roiter–Salmerón 的两个经典结果——代数存在乘法基，以及特征不为 2 时的标准性。作者声明最初由 GPT-6 Astra 生成证明，随后 Claude Opus 5.5 和 Gemini 4 Argon 多轮修订；自己尚未完全理解全文，计划花费数周至数月审阅。Hexagon 关联 PALOMAR-2026-10-23-000004 登记，但注册事实不等于所有外部文献依赖与非形式数学陈述均已由无关联专家确认。结论本身为经典已知定理，事件的新意在 AI 生成的另一条证明路线及形式化登记，不应被报道为 AI 首次发现乘法基定理。
形式化数学
推荐理由：著名结构性代数定理得到 AI 主导的新证明框架，连同可追踪登记和公开的人类理解缺口，为验证大模型自动数学重证明质量提供重要案例。
08:00
Andrew Riesen & David E. Evans / Hexagon 精选 AI 评分 95 ☆ Andrew Riesen 与 David E. Evans 于 10 月 23 日公开构造性量子代数手稿：对每个奇数 N≥3，给出带 Haagerup–Izumi 融合规则的球面融合范畴及具有明确模性质的顶点算子代数，使后者模范畴等价于前者的 Drinfeld 中心。研究使用 Virasoro 扩张、共形移位的 E7 格顶点代数与 simple-current extension，声称所得模型有中心荷 −6N²−10、有效中心荷 8 与 N²+3 个不可约模。作者披露 AI 参与发展论证和撰写大量文本，人类作者修订整理，但部分 AI 辅助推导尚未完成独立人工验证；未声称整篇已由 Lean kernel 形式证明或经过同行评议。
数学发现
推荐理由：AI 进入高阶融合范畴与 VOA 构造研究，得到对所有奇 N 的结构性数学对象和可检查的数值不变量，且保留具体的未复核论证风险。
08:00
Deep Bhattacharjee / Hexagon / GitHub 精选 AI 评分 96 ☆ Deep Bhattacharjee 于 10 月 23 日公开两篇紧密关联的格论研究，针对 Adaricheva 等人的最大子格补集结构猜想。第一篇使用一个 14 元半分配格的平方中的 26 元子格，构造补集具有两个最小元的极大子格，否定补集总是区间的推广。第二篇给出凸维数为 3、4 的凸几何反例及 10、11 元有限例子，进一步反驳其关于共享最小元区间并集的若干假设与问题。作者说明 Claude Opus 5.5 借 Claude Code 搜索构造、编写复核程序、Lean 4 证明及论文草稿，提供版本化代码与精确枚举；作者批准最终版，尚无 Radar 独立运行 Lean 或专家审稿。两篇构成同一结构理论反例系列，关联原始论文 https://hexagonmath.org/2610.00495v1。
形式化数学
推荐理由：有明确小规模结构、一般性结论和作者报告的 Lean 证明工件；将一条研究链中的紧密相关反例归并避免按每个预印本重复计数。
08:00
Deep Bhattacharjee / Hexagon / GitHub 精选 AI 评分 95 ☆ Deep Bhattacharjee 于 10 月 23 日公开两篇关于 Graffiti.pc 计算机辅助猜想集 Written on the Wall II 的图论反例。其一针对 Conjectures 319、352、358、359、427，给出 caterpillar 与 complete-graph 拼接产生的无限反例家族，部分参数差距无界；其二否定 Conjecture 66 关于连通图最大诱导森林数的平均度与补图度数众数下界，并声称对不同定义解释均构造无界违反。两篇均由作者选题与定稿，Claude Code/Opus 5.5 参与发现、精确枚举、checker、Lean 4 证明和初稿，已有版本化代码发布。尚未由 Radar 独立重跑程序或进行专家验证；作为同一 Graffiti.pc 主题系列合并为一条事件，另一来源为 https://hexagonmath.org/2610.00501v1。
形式化数学
推荐理由：AI 助力批量检验经典计算机生成图猜想，并从有限反例提升到全参数无限家族及可审计 Lean/程序证据；分组明确减少同一天近似重复新闻。
08:00
Deep Bhattacharjee / Hexagon / GitHub 精选 AI 评分 94 ☆ Deep Bhattacharjee 于 10 月 23 日研究 Sahbi 的 k-star-forming / k-independence 猜想，报告对每个 k≥3 构造 3k+3 个顶点的连通二部图，满足 β_k=2k+2 而 upper star-forming 数至少 3k，否定二部图一般等式；同时证明链图的等式对所有 k 成立，并将二部图 minimal 2-star-forming 集合大小判定问题证明为 NP-complete。Claude Code/Opus 5.5 负责搜索、程序、Lean 4 证明和初稿，作者指导并批准；公开版本化源码，但没有独立专家审稿。原文还提及相关前期公开的小参数反例，因此本记录主要是全 k 家族与复杂性结论的新发表，而非首个小实例。
形式化数学
推荐理由：同一数学问题同时区分反例范围、仍成立的重要图类和计算复杂性，并保留 AI 生成证明与作者形式验证声明边界。
08:00
Deep Bhattacharjee / Hexagon / GitHub 精选 AI 评分 93 ☆ Deep Bhattacharjee 于 10 月 23 日发布具体图论反例：选取 octahedron 与一个 21 顶点、Grundy domination number 为 10 的图 H，其强积具有至少 21 的 Grundy domination number，因此不能满足原猜想的乘法关系 γ_gr(G⊠H)=γ_gr(G)γ_gr(H)。论文针对 Brešar 等人的 Conjecture 22，并提供显式图、搜索程序和作者声称的 Lean 4 证明；Claude Code/Opus 5.5 负责计算、证明程序和初稿，作者审批最终结论。该反例不是对其他 domination 变种乘法性质的全盘否定，尚无独立审稿。
形式化数学
推荐理由：小规模、目标明确的猜想反例配有公开有限计算和形式证明工件，具有可复核的数学增量。
08:00
Deep Bhattacharjee / Hexagon / GitHub 精选 AI 评分 93 ☆ Deep Bhattacharjee 于 10 月 23 日在 Hexagon 公布关于三维 Morley 四面体构造的 AI-assisted 反例：研究 Tran 将二等分/三等分面推广至 p-secting planes 后提出的 Conjecture 8.6，并对坐标盒 [−a,a]×[−b,b]×[−c,c] 中等腰四面体给出其 Morley 导出四面体为正四面体的几何充要条件。当 a,b,c 两两不同时得到不满足所谓四条相等交叉棱的具体反例，同时报告四等分取 e=f=g=4 的特殊结论。Claude Code/Opus 5.5 参与计算搜索、验证程序、Lean 证明与初稿，作者审批最终版；尚未独立复跑工件或审稿。
形式化数学
推荐理由：体现 AI 辅助几何构型搜索不仅发现孤立实例，还推进至参数化证明与例外情况分类；明确区分作者报告的 Lean 工件与独立审查。
08:00
Deep Bhattacharjee & Ushashi Bhattacharya / Hexagon / GitHub 精选 AI 评分 94 ☆ Deep Bhattacharjee 与 Ushashi Bhattacharya 10 月 23 日发表其较早 Geometric Selection Conjecture 的 AI-assisted 修正分析。作者原本要求 Claude Code 证明镜像对称不变、唯一选择物理可行真空的猜想；模型指出其中若干条件依赖实测数据，不能直接按数学定理封闭，转而提出镜像固定可行真空不可能存在的命题：若真空与其 mirror 等价，则相关 Calabi–Yau 三重态 Euler 数与丛的第三 Chern 类满足零约束，从而不能产生净手征代数族。提交者报告 Python 程序在相关离散配置上执行 511 项检查，代码作为 v1.0.0 release 公布；没有整项 Lean end-to-end 形式化，也不代表完整物理景观选择问题得到解答。
数学发现
推荐理由：AI 不仅生成证明，也能在原始目标不适当时识别概念性矛盾、重新提炼可检验的较窄数学陈述，是 Agentic Science 科学方法学的代表性案例。
08:00
Bingo Baggins / Hexagon 精选 AI 评分 92 ☆ Bingo Baggins 于 10 月 23 日首发 AI 生成的概率分析研究，延续其较早关于 heat-evolved Weyl polynomials 实根化时间极限的论文，提出可量化的新结果：在 t≥1+ε 的区间内分布收敛可达到任意 α<3/50 的 n^(−α) 速率；在共享最高次数系数的耦合下给出 O(1/n) 的实根化时间误差及 final collision 位移的尾概率估计。论证依赖 Hermite 多项式与随机高斯幂级数非实零点分布。Hexagon 明确标注文字主要由 AI 生成、贡献者没有理解证明的部分，未给出独立人工检查或完整形式化证书；本条仅作为带新速率/尾界的未证实后续研究主张，不将 10 月 22 日已有基础极限论证重新定日。
数学发现
推荐理由：与前一天关于随机 Weyl 多项式的首篇工作相比新增定量收敛和尾部分布界，属于有新数学内容的 follow-up；但人类理解程度低，作为低验证等级研究主张明确标注。
08:00
Idris Ali Shaik / Hexagon / Palomar 精选 AI 评分 91 ☆ Idris Ali Shaik 于 10 月 23 日公开一项逻辑与形式验证研究，分析 c432 优先级控制器任意规模扩展在指定首阶段 bridge fault 下的可达 qualifier 集合，并对特定 guarded decoder 子类给出线性复杂度检测算法、完整 CNF 不可满足实例的 O(N³) resolution refutation 界，同时报告检测问题 P-complete、最小集优化 NP-hard、计数 #P-complete 等结论。OpenAI Codex 协助发现论证、Lean 形式化和手稿准备，人类作者逐项审核承担责任；页面链接 PALOMAR-2026-10-19-000010，故其**首次 Lean 登记是 10 月 19 日，不是 23 日**。本条记录 23 日首次公开的完整研究论文，而非新登记或无条件验证所有复杂度证明。
定理证明
推荐理由：把辅助形式化与精确可达集、proof-complexity 联系到实际自动测试生成，且公开形式化范围与先前登记日期；保留为形式验证交叉方向的精选边缘事件。
10月22日 ⌄ 星期四 · 16 条
08:00
Christopher Frei & Wataru Kai / Hexagon 精选 AI 评分 98 ☆ Christopher Frei、Wataru Kai 于 10 月 22 日首次公开短文，声称将 Kerr 对 OpenAI 先前 Dirichlet L 函数 Landau–Siegel 零点论证的变体推广至 Hecke L 函数，得出不存在 exceptional zeros 的结论。作者明确说明本文数学和文本完全由人类撰写、没有使用 AI，提前公开是因 OpenAI 数论证明引发关注，计划并入另一个正式工作。此条是人类数学家基于 AI 数论结果衍生出的新推广，不应归因于 AI 直接推导，也未等同已完成正式同行评审。
数学发现
推荐理由：OpenAI 最初数学成果获得真正独立的人类推导，并延伸至更广的 Hecke L 函数语境，是对 AI 数学研究价值与专家承接能力的重要实质检验。
08:00
Chih-Yao Wu / Hexagon / GitHub 精选 AI 评分 98 ☆ Chih-Yao Wu 于 10 月 22 日发布关于任意五个正质量牛顿质点的平面中心构型有限性的研究主张，尝试补齐 Albouy–Kaloshin 既有定理的特殊质量情形。论证结合 singular diagrams、能量及力矩约束、复代数方程退化分析、有限多项式选取和例外情形精确证书；仓库附 Lean 形式化与英文审查指南。作者披露数学论证、Lean 代码和手稿均由 AI agents 主导，曾在 10 月 6 日向专家发送初稿但完整独立专家审查尚未结束。本条只记录 10 月 22 日正式公开的研究声明，不把 Smale 第六问题整体或五体中心构型研究所有版本视为已获同行确认。
数学发现
推荐理由：涉及经典天体力学中心构型有限性困难问题，并公开大模型生成证明与 Lean 材料；验证程度和几何命题本身的范围被明确保留。
08:00
Troy Winarski / Hexagon / GitHub 精选 AI 评分 98 ☆ Troy Winarski 于 10 月 22 日公开对 Q(√−3) 上满足单位相容条件的角 Hecke L 函数的形式证明研究：报告所有相容角类型及单位范数实扭曲在严格 Re(s)>15/16 半平面内无零点，主极点另行排除；改进此前 Re(s)>23/24 的角角色家族结论。原文指向冻结 Lean 工件、statement comparison、axiom audit、递归 kernel replay 与商对象 postchecking，且如实说明继承 OpenAI Family 003 的部分技术来源引理尚待独立重构，并明确称为 xenoproof 而非人类独立认证。Radar 未自行重放仓库，不能将作者形式化报告等同第三方数学专家审稿。
形式化数学
推荐理由：有明确改进幅度、完整的审计证据分层和对形式化正确性与人类理解的严格区分，是 AI4Math verification-first 工作流的重要样本。
08:00
Deep Bhattacharjee / Hexagon / GitHub 精选 AI 评分 97 ☆ Deep Bhattacharjee 于 10 月 22 日公布关于 Lehmer's totient problem 的新排除范围：若复合数 n 满足 φ(n)∣n−1，则其不同素因子至少有 16 个；论文进一步对 (n−1)/φ(n)≥3、3∣n 等情形给出更强限制，并检查 φ(n)∣n+1 的小因子例外。Claude Code 负责搜索、证明程序、部分不依赖搜索的 Lean 证明及初稿，作者审核修改。关键有限检查由独立编写的 Python 与 PARI/GP 程序执行且有日志。**Lehmer 猜想本身仍未解决**；形式化仅覆盖指定推导，计算证书不等同全部无条件 Lean 证明。
数学发现
推荐理由：具有真实数论下界改进及两种程序交叉检验的强可复算证据；同时避免将更严格的有限排除范围误报成著名猜想最终获证。
08:00
Deep Bhattacharjee / Hexagon / GitHub 精选 AI 评分 95 ☆ Deep Bhattacharjee 于 10 月 22 日公开 regular tournaments 的随机 blow-up 中 Wormald 的 Hessian 行列式研究：用 skew adjacency matrix S 给出 H=d det(d²I+S²)/det(d²I−S²)，并报告证明 H≠0 和 d/H 为有理数平方；对 cyclic tournament 得到相应常数趋于 cosh(1)/cos(1)≈2.85596，涉及 Wormald 的两项猜想。Claude Code 运行搜索与计算、编写 checking programs 与 Lean 4 证明，作者负责最终稿；已公开代码版本与纸面证明，但没有声称无关联数学专家已完成审查。
形式化数学
推荐理由：将组合学中两个清楚编号的猜想转化为矩阵恒等式和公开可重算形式证明工件，比仅宣布 AI 发现有更高可检验价值。
08:00
Deep Bhattacharjee / Hexagon / GitHub 精选 AI 评分 97 ☆ Deep Bhattacharjee 于 10 月 22 日报告精确计算 book Ramsey number R(B_57,B_58)=231，构造 230 顶点二分块 circulant graph 使其不含 B57、补图不含 B58，结合已有 Rousseau–Sheehan 上界封闭该实例。Claude Code 产生构造、C/Python 独立检查以及 Lean 4 形式化；作者称纸面论证可化为 Z115 上 57 项不等式，核验程序枚举 26,335 个点对，Lean kernel 以 decide 而非 native_decide 校核目标。只证明该特定 Ramsey 数，并未解决 Wesley 一般猜想；本轮没有自行运行 Lean。
形式化数学
推荐理由：新精确组合数值具有多层可审计证据：显式图、独立程序及可编译的 Lean 声称，是 AI-assisted finite mathematics 高价值案例。
08:00
Deep Bhattacharjee / Hexagon / GitHub 精选 AI 评分 95 ☆ Deep Bhattacharjee 于 10 月 22 日公开 F3 上矩阵空间研究：报告任何六维的 3×3 矩阵子空间必包含非零幂零矩阵，因此 nilpotent-free 空间最大维数为 5，与 Wigderson 对一般域的预期维数 6 冲突。Claude Code 参与搜索、验证程序、论文和 Lean 4 形式化；形式证明核心使用 native_decide，同时另有两份 C 程序复核有关有限枚举。该结果是对 F3,n=3 的反例，不直接证明所有其他域或维数中的最优界；尚无独立数学专家审稿声明。
形式化数学
推荐理由：一个小参数但能确切推翻全称矩阵空间猜想的案例；native_decide 与独立 C 程序同时披露，有利于检查证明技术信任边界。
08:00
Deep Bhattacharjee & Ushashi Bhattacharya / Hexagon 精选 AI 评分 95 ☆ Deep Bhattacharjee 与 Ushashi Bhattacharya 于 10 月 22 日公布四维代数几何的反例主张：1389 可作为 terminal Calabi–Yau 四维簇及四维 log-canonical 奇点的指数，但不是任意四维 canonical 加权射影空间的 Fano 指数，因而违背 Liu 的相关猜想。研究者说明 Claude Code 完成搜索、程序、Lean 4 证明和初稿，两名人类作者最终审阅。公开 release 包含程序和形式化材料；某个参考资料中的 Zenodo DOI 占位符不应当被当成已核验的真实存档链接。本轮未独立重跑 Lean 或确认正式同行评议。
数学发现
推荐理由：具体反例足以改变一个全称代数几何主张，且参数及模型角色公开；对 AI-discovery 记录须保持复核和来源完整性限制。
08:00
Deep Bhattacharjee & Ushashi Bhattacharya / Hexagon / GitHub 精选 AI 评分 94 ☆ Deep Bhattacharjee、Ushashi Bhattacharya 于 10 月 22 日公开对整数贪心 Fibonacci–Lucas 表示的研究：声称证明 Zeckendorf 表示中的项数总和与 greedy Fibonacci–Lucas 项数总和的比值趋于 (5−√5)/2，并解决 Kimberling、Greathouse 与 Kurkov 相关 OEIS 猜想。Claude Code 完成搜索、检查程序、Lean 4 证明和初稿，两名作者批准最终版，并提供程序数据的版本化 release。区别渐近定理的正文证明、Lean 证明声称和可能仍需独立专家评议的状态。
形式化数学
推荐理由：对有出处的多个整数序列猜想给出统一渐近常数和核验工件，是 AI-assisted enumerative number theory 的可跟踪进展。
08:00
Benjamin Severn / Hexagon / Zenodo 精选 AI 评分 95 ☆ Benjamin Severn 10 月 22 日公开 AI 主导的代数几何手稿，声称对 K=Q(i)、Hermitian discriminant [-3] 的极化 Weil 型阿贝尔六维簇，所有 Weil 类都是代数的；在 Hodge 群为完整 special unitary group 时，所有幂上的 Hodge 类亦为代数的。论文使用具有 W(E8)·μ4 monodromy 的曲线覆盖与具体秩计算，并归纳相关代数循环生成机制。Claude 模型完成大部分推导及 GAP/SageMath/Python 证书，OpenAI GPT-6 Astra/GPT-5.6 Sol 用作跨模型对抗审阅；**AI 间交叉评审不等于独立人类专家审稿或完整 Lean kernel 证明**。这是限定族的研究主张，不是 Hodge 猜想整体解决。
数学发现
推荐理由：重大但严格限定的 Hodge 理论进展，计算工件及多模型交叉验证均公开，同时清楚说明尚未获得独立人类专家的数学确认。
08:00
John Tripodo / Hexagon / Zenodo 精选 AI 评分 94 ☆ John Tripodo 于 10 月 22 日提交稀疏二元矩阵行列式研究：对密度参数 r=3,…,14 提出明确的 affine-exponential 行列式上界，在总 1 元素数 e≤rn 下取得射影平面 incidence matrices 对应的指数率并刻画取等情形，不要求逐行/列度数均匀。该研究披露 OpenAI 工具深度参与证明工程和精确计算，伴有有限实标量证书、无界度数尾项控制与 98 模块冻结 Lean 工件。作者明确说明没有外部专门数学审查，也不声称最近一次 fresh Lean compilation 已完成；不能把工件存在直接升级成 Radar 的独立复现结果。
形式化数学
推荐理由：将非常规稀疏矩阵估计转成精确计算与形式证明可追溯工件，并披露证明复跑与人类理解方面的限制。
08:00
John Tripodo / Hexagon / GitHub 精选 AI 评分 93 ☆ John Tripodo 于 10 月 22 日公开 double Hall property 二部图的渐近最优最大度证明主张：最小可能最大度与 √(2n) 渐近等价，给出同时对两个 shores 成立的确定性规则二部图构造，度数不超过 √(2n)+O(n^(21/80))。作者表示 OpenAI tools 参与数学探索、程序核验、撰稿和形式证明，有限误差估计调用已发表 Baker–Harman–Pintz 素数短区间结果，形式转移保留其为显式假设。无外部同行审稿、无最近 fresh Lean 编译主张，论文不是独立发明相关经典素数分布引理。
数学发现
推荐理由：AI 帮助给出可量化的渐近最优图构造，公式明确且依赖外部深层定理的边界透明，具有超出单个例子的结构性价值。
08:00
Deep Bhattacharjee / Hexagon / GitHub 精选 AI 评分 95 ☆ Deep Bhattacharjee 于 10 月 22 日公开由 Claude Code 主导搜索与证书生成的低维拓扑数据项目，针对至多 13 个交叉点的 KnotInfo 未决条目研究 bridge index、meridional rank 与 smooth nonorientable four-genus。作者公开 243 项 bridge-index 证书、2728 项 pinch move 证书、382 项格嵌入下界及相互独立的验证程序，使用 SnapPy、Regina 与精确枚举，并保留未定项目范围。Hexagon 摘要中的某些总数以尚未展开的 LaTeX 宏表示，Radar 不猜测具体新解决条目数量；证书由提交者编写的 checker 验证，尚非无关联专家全量审计。
形式化数学
推荐理由：大规模数学数据库难例的有限证书积累与独立复核程序协作，展示 AI 可以产出大量可单项验证的真实数学工件而不仅是文稿。
08:00
Deep Bhattacharjee / Hexagon / GitHub 精选 AI 评分 94 ☆ Deep Bhattacharjee 于 10 月 22 日发表关于长度 n 的 binary circular words 中 distinct abelian squares 数量的研究，报告下界 ⌊(n−1)/2⌋ 并完整分类取等词，修正 Simpson 猜想在特定偶数长度时遗漏交替词 (ab)^(n/2) 的部分。Claude Code 参与检索、证明、Lean 4 工件与程序核验，作者称六项主要结论均在 Lean/Mathlib 内闭合，且由 C、C++、Python、Julia 等多实现检查小规模情形。本轮不将有限实例检查误写为无限情形的机器独立证明。
形式化数学
推荐理由：兼具一般计数定理、对现有猜想精确纠错和多工具证据，是 AI-assisted formal combinatorics 适合精选的实例。
08:00
Deep Bhattacharjee / Hexagon / GitHub 精选 AI 评分 93 ☆ Deep Bhattacharjee 于 10 月 22 日报告证明 Hou–Zhao 关于 Welch 幂函数 X^(2^m+3) 在 F_(2^n)、奇数 n≥7 情况下不是 third-order sum-free 的猜想：利用 binary Kloosterman sum K_n 给出允许零和三维仿射子空间的精确计数 (2^n+1−3K_n)/4，并用 Weil 界推出正性。Claude Code 完成辅助检索、推导与多语言验证程序；Lean 4 仅形式化若干代数恒等式及 n=5,7 的有限证书，**未声称所有 n 的分析论证都被 Lean end-to-end 核验**。
数学发现
推荐理由：密码学相关有限域函数猜想得到具体公式及手写证明、程序检查和有限 Lean 证据，且不会混淆局部 kernel check 与无限参数结果。
08:00
Deep Bhattacharjee & Ushashi Bhattacharya / Hexagon / GitHub 精选 AI 评分 94 ☆ Deep Bhattacharjee 与 Ushashi Bhattacharya 于 10 月 22 日报告：在 R⁵ 中球心限定为同一个格的两个平移陪集的周期球堆积，密度不超过 D5 格堆积；在同构意义下有三个等密度取等家族，包含 Leech 层状构型与 Szöllősi kissing configuration。Claude Code 参与枚举、精确检查程序、Lean 4 证明与文稿，作者批准最终版。证明中的 ray-list 完备性依赖精确计算枚举并提供 release；仅对 two-translates-of-lattice 受限类别成立，**不是五维所有可能非周期球堆积的全球最优性定理**。
数学发现
推荐理由：对五维经典难几何对象给出定量分类和精确计算工件，限定范围清晰且便于后续独立复核。
10月21日 ⌄ 星期三 · 9 条
08:00
Tristan Buckmaster / Terence Tao blog 精选 AI 评分 93 ☆ Tristan Buckmaster 于 10 月 21 日在 Terence Tao 的博客发表文章，结合 AI 辅助 Euler / Navier–Stokes 研究的竞争经验，讨论青年研究者在前沿模型算力高度不对称、未发表数学想法通过商业模型泄露、论文优先权奖励机制失效时面临的处境。文章具体倡导高校级 AI 服务协议、零数据保留与使用审计、训练数据明确 opt-in、由学术界控制的开放权重研究基础设施，以及更加奖励数学理解、可读阐释和共享资源的贡献体系。这是作者观点与治理建议，非已经采纳的学会准则、法律或技术发布；与 10 月 18 日 Maggi 的宏观讨论有重叠，但新增明确面向研究生和博士后的权益与保密机制。
工具与生态
推荐理由：由积极参与 AI-assisted 数学发现的数学家提出针对下一代研究者的实际保密与贡献认可方案，是可定位的 AI4Math 共同体治理讨论；收录范围严格限定为 10 月 21 日首发的意见文章，而非已经生效的制度。
08:00
Jungang Chen / Hexagon 精选 AI 评分 97 ☆ Jungang Chen 于 10 月 21 日连续公开两篇相互关联的拟阵 Tutte 多项式研究。第一篇以秩 32、64 元素的连通自对偶且可有理表示的拟阵，给出两个基覆盖下 max{T(2,0),T(0,2)}<T(1,1) 的精确整数反例，并构造相应比值趋于 0 的无穷家族。第二篇给出任意指定 k≥3 连通的可表示拟阵，使乘积版 Merino–Welsh 比值无界，包含 1011 元素的有限计算实例，并排除若干控制 girth/cogirth 条件下的猜想；未声称推翻图拟阵或二元拟阵的所有版本。作者披露 GPT-6 Pro 在构造、证明与代码中发挥实质作用；精确整数检查及模型协助重算并不代表独立专家审核或 Lean 形式证明。关联原稿：https://hexagonmath.org/2610.00430v1。
数学发现
推荐理由：同一日期的两个基覆盖/连通性相关 Tutte 不等式反例被合并为一条研究系列事件，保留精确计算与未获独立人工检查之间的证据差异。
08:00
Jungang Chen / Hexagon 精选 AI 评分 95 ☆ Jungang Chen 于 10 月 21 日公开另两篇 AI 辅助组合学反例研究。针对 Csikvári 的置换 Tutte 多项式不等式，他构造最小度与点连通度均可任意高的平衡二部图族，两个轴值乘积趋于 0，并给出 1000 顶点精确有理数证书。针对 Ok 关于 Tutte 多项式删边比值的三项猜想，文稿给出 16 顶点平面 chordal 2-tree 和五边 diamond 图的显式违反案例，并推广到高连通图族。两篇贡献于同一 AI-assisted 反例探索，但**不等价于推翻所有 Merino–Welsh 图/拟阵原始不等式**；代码精确计算、AI 内部审查不代表已完成 Lean 或人类专家独立复核。关联原稿：https://hexagonmath.org/2610.00431v1。
数学发现
推荐理由：一组可检查的结构性反例使多个具体提出的图多项式不等式受到挑战，精确数值和一般家族兼备；按两个高度相关的研究问题合并，避免四篇投稿四次计算事件。
08:00
Qiyue Tang / Hexagon 精选 AI 评分 96 ☆ Qiyue Tang 于 10 月 21 日首发关于 weakly Gorenstein symmetry conjecture 的 AI-generated 反例：声称存在 29 维代数左 weakly Gorenstein 而右侧不满足，并进一步给出一个 145 维 gendo-symmetric 代数，两例适用于包含无限乘法阶元素的域。作者表示通过约三小时 GPT-6 Astra Pro 对话得到构造，之后使用 Codex 与 Rethlas-OSV（仍为模型协助）审核，并主动邀请独立专家检验。投稿没有完整 Lean 证明或独立人类数学审查，不可将该猜想已被学界证伪作为事实。
数学发现
推荐理由：有具体代数维数、左/右非对称性质和直接关联原始猜想的高潜力数学主张，且披露 AI 主要角色与未经独立审核状态。
08:00
RJ Acuna / Hexagon / GitHub 精选 AI 评分 94 ☆ RJ Acuna 于 10 月 21 日公开使用 Claude Fable 辅助的数论成果：给出 Petrov 关于任何代数数可实现为某个整数系数多项式临界值的独立构造证明，补充可实现多项式的分类和次数下界，并公布 Lean 4 形式化与在线计算器。作者称自己理解全部证明内容。**临界值覆盖代数闭包本身是早有 Petrov 论证的已知定理**，本事件记录新的独立证明、可复用形式化和构造性工具，而非 AI 首次发现该结论。10 月 21 日同日出现 v1 与 v2，以最新 v2 作为原始页面。
形式化数学
推荐理由：经典结果产生 AI 辅助的独立人类可理解证明、Lean 代码和交互计算工具，是文献与自动形式化共同推进的实用实例；不重复计算数学定理首次发现。
08:00
Michael Mislan / Hexagon / Palomar 精选 AI 评分 94 ☆ Michael Mislan 于 10 月 21 日公开化学遗传模型研究：在四个隔室、三类竞争燃料的催化剂系统中，研究有限供给与停止播种后的分裂继承过程，给出失败概率不超过约 0.004518 的定量证明，并研究 4000 分子规模下连续 100 次模板外复制恢复的成功概率至少 0.999。作者与 AI 系统共同开发证明、数值证书和形式化；主有限库存定理与当日 Palomar 登记 PALOMAR-2026-10-21-000010 关联，但第二个协同恢复结果仅有传统数学证明，**不是所有化学/进化断言均经过 Lean**；本文并未证明现实生命起源或开放式演化。
形式化数学
推荐理由：概率过程、有限资源与 Lean/Palomar 证明工件结合，具有可检查的定量结果和清晰的形式化范围；界限明确局限于提出的数学化学模型。
08:00
Michael Mislan / Hexagon / Palomar 精选 AI 评分 92 ☆ Michael Mislan 于 10 月 21 日连发两篇自催化反应网络研究，给出特定可逆 Type II_l 核心在严格正降解下及与 Type V 网络在非负降解下的正稳态唯一性定理，同时构造去除 source-minimality 等条件后会出现两个稳态的有限反例。文稿主要由 AI 辅助开发，部分数学由人类理解；页面连接 Lean 证明与 Palomar 登记。**这些形式化工件分别在 2026 年 9 月 25 日与 9 月 30 日已经登记**，因此 10 月 21 日仅收录当日首次公开的完整论证系列，绝不声称当日首次 kernel check。关联：https://hexagonmath.org/2610.00439v1。
形式化数学
推荐理由：将同一反应网络稳态结构的两篇紧密互补手稿合为一个发表里程碑，明确区分已存在的 September 机器证明与新公开的 October 数学整理。
08:00
Michael Mislan / Hexagon 精选 AI 评分 92 ☆ Michael Mislan 于 10 月 21 日公布两篇研究特定化学反应网络数学判据的 AI-assisted 手稿。第一篇构造可逆自催化网络反驳仅依赖总体化学计量种子比的最优亲和力下界，并提出记录动力学响应信息的替代 capacity；第二篇使用正有理双分子网络反例说明稳态环中零因子并不是 absolute concentration robustness 的无条件充要条件，进一步给出带明确代数假设的 block-compatible completeness 界面。两文均报告选定反例和精确证书已形式化；其他几何/非线性论证仍为传统手稿内容。**页面引用的 Palomar 注册时间为 2026 年 9 月 30 日与 10 月 1 日**，不能据此虚构当天新的形式核验证书。关联：https://hexagonmath.org/2610.00441v1。
形式化数学
推荐理由：两篇相关的模型判据修正均包含明确假设、可计算反例和限定范围的形式化主张；合并收录避免将单一 AI-assisted 模型系统的近重复证据过度计数。
08:00
Daniel Adam Pyle / Hexagon / GitHub 精选 AI 评分 92 ☆ Daniel Adam Pyle 于 10 月 21 日公开 AI-powered assistant Lyra 主导的图论研究，声称 Fibonacci cubes 与 Lucas cubes 的 total mutual visibility number 均按 ρ^n/n 同阶增长，其中 ρ³=ρ²+1；论文分析可识别纤维分解、最短路径与 open packing 的联系，给出维数 20 / 16 以内的可重算枚举和部分常数界。作者主动披露数学研究、程序与文稿由 AI 生成，人类尚未完整理解，检查主要为其他 AI 与精确整数计算；没有 Lean 核验证明或独立同行审查，也没有求出最终精确渐近常数。
数学发现
推荐理由：围绕有明确数列和几何组合含义的图族给出可量化研究主张与源码，并完整披露 AI 主导及人工审查限制；相比简单参数枚举包含更强的结构性渐近命题。
10月20日 ⌄ 星期二 · 12 条
08:00
Terence Tao / What's New 精选 AI 评分 97 ☆ Terence Tao 10 月 20 日公开发起 Math 2.0 风格的开放协作问题：对近期排除 Landau–Siegel 零点的各种新论证，允许披露 AI 参与，尝试导出假设存在的第十个类数一虚二次数域判别式的显式上界，并比较方法优劣或改进常数。挑战强调自查、可重用的数学理解和非抢先竞赛；可接受没有达到最优界的负结果。其基准类数一问题早已解决，公告是可量化评估 AI 数学推理与协作的新研究挑战，既非新证毕数论定理，也非 Lean 形式化成果。
工具与生态
推荐理由：以公开、可比较的数论中间目标替代模糊的 AI 数学能力声明，同时明确 AI 使用披露、复核与协作规则，是 AI4Math 研究生态中的可操作新机制。
08:00
Chen & Huang / arXiv 精选 AI 评分 98 ☆ Bocong Chen、Jing Huang 于 10 月 20 日首发 34 页论文，声称对所有偶数阶有限域 F_q 的非平凡线性 [n,k] MDS 码证明长度界 n≤q+1，仅 k=3 或 q−1 的例外允许 n≤q+2。证明结合 tangent-envelope 多项式、Reed–Solomon 对偶码与三变量 Artinian Gorenstein Hilbert 函数的单峰性。作者披露 ChatGPT 用于证明策略探索、中间计算检查与编辑，数学责任由作者承担；论文亦引用 Kumar 于 10 月 15 日公开的另一份配 Lean 登记的独立论证。当前这篇手稿未报告完整 Lean 形式化或外部正式同行评议，因此记录 10 月 20 日新增的独立论证，而非宣告猜想已获学界公认解决。
数学发现
推荐理由：经典编码理论和有限几何问题出现具有独立证明路线的 AI-assisted 论文，且与较早机器核验证书形成可对照的独立研究增量；保留论文主张与专家审查的区别。
08:00
Gregory V. Chudnovsky / arXiv 精选 AI 评分 98 ☆ Gregory V. Chudnovsky 于 10 月 20 日向 arXiv 首次公开提交与 ChatGPT 联合完成的数论研究：在 OpenAI 2026 年 9 月 π 无理性指数工作的行列式与插值方法基础上，处理代数参数对数、共轭匹配、独立有理对数商的上界（三的指数上界）以及分级 Padé 逼近。论文说明先前 Liu–Jiang–Zhang 已获得部分对数值结论，因此不独占旧成果优先权。附带 Lean 源码和复现说明；62 项编号结果中有 53 项为直接端点或组合检查、另 9 项应用依赖具名经典数学定理作为输入，不能称整个手稿及所有底层定理均被独立完整形式验证。
形式化数学
推荐理由：一流数论作者把 AI 辅助的新结果、精细文献归因、62 项编号结论的形式化核验边界及可读的 Lean 端点审计共同公开，为区分 mathematical theorem、checked endpoint 与 assumed classical input 提供重要范例。
08:00
Kaarel August Kurik / arXiv 精选 AI 评分 95 ☆ Kaarel August Kurik 10 月 20 日首发研究：对实 Banach 空间 X、Y，若单位球之间的非扩张映射 F 将源单位球面映入目标单位球面、且其像覆盖目标球面，则 F 必是一个满射线性等距的限制。论文以量化刚性引理和 Baillon–Bruck 渐近正则性为核心，并得出单位球等距映射的极点结论，回答 Bargetz、Dymond、Pirk 的有关问题。arXiv 注明证明研究使用 AI 语言模型，定理 1 和引理 2 提供 Lean 形式化链接；并未宣称整篇论文每一个推论已被 Radar 复现或得到独立审稿。
形式化数学
推荐理由：存在精确新数学命题、明确 AI 贡献披露及对应核心定理的形式证明，比只凭模型输出宣布解决泛函分析问题具有更强可查证性。
08:00
Thomas Bloom & Wouter van Doorn / Hexagon 精选 AI 评分 96 ☆ Thomas Bloom 与 Wouter van Doorn 于 10 月 20 日在 Hexagon 发布纯人类撰写的证明阐释和局部简化，针对 OpenAI 10 月 6 日公布的单位分数研究，论证任意 0<a/b<1 可由 O(log log b) 个互不相同单位分数组成，并研究 1 被 k 个不同单位分数表示的双指数数量级。论文明确归因原始 AI-generated 证明，并通过人类独立行文解释其数学内容；本条记录新的人工阐释与审读里程碑，不把早前数学主张重新定为 10 月 20 日首次发现，也不等于整个 OpenAI 论文集已获正式同行评议。
工具与生态
推荐理由：数学家对具体 AI 生成研究进行逐步人工重写与简化，是独立于初始模型输出的理解证据，并可成为 AI4Math 科学验证标准的代表案例。
08:00
Shawn Krisman / Hexagon 精选 AI 评分 97 ☆ Shawn Krisman 于 10 月 20 日在 Hexagon 发布由 Claude Code / Claude Opus 5.5 主导撰写与形式化的数论研究，主张 Legendre chi 函数 χ₂(1/3)、χ₂(1/5) 均无理。核心使用 Hankel 行列式、素数逐项分母界、离散 log-gas 大小估计与模辅助素数非消失条件。提交者声称将所需素数定理和数值证书也在 Lean 4 / Mathlib 内闭合、仅使用标准公理；Hexagon 标注 human understanding 为 no parts。Radar 未独立编译源码或审查 informal/formal statement correspondence，不将提交者的 kernel-checked 声明等同独立数学认可。
形式化数学
推荐理由：主要由 AI 完成的新无理性研究给出明确目标、分析证明与可查验形式化主张，可用于比较机器内核证据、人类理解和独立复核的不同层级。
08:00
Sean Litsey / Hexagon 精选 AI 评分 96 ☆ Sean Litsey 于 10 月 20 日公开主要由 Claude Opus、Sonnet、Haiku 5.5 Agent 在 Claude Code 中生成的数论结果，报告 μ(G±5π²/48)≤38.35、μ(L(2,χ₋₃))≤23.82；对于后者，相比作者所引以前的有效界 μ≤24781 大幅改进。其方法由 OpenAI 的 Catalan 常数行列式工作衍生，结合 p-adic 分母估计、Jacobi 矩阵与离散能量界；论文声明所有主结果均以 Lean 4 形式化，没有未证明步骤且仅依赖标准公理。公开声明 human understanding no parts，尚缺 Radar 的实际 Lean 重放与第三方专家核查。
形式化数学
推荐理由：显示多模型 agent 对已有 AI 数论技术作可量化数学改进，并附声明的完整 Lean 证明；但仍保持 claimed formalization 与独立复现证据界限。
08:00
Ralf Stephan / Hexagon / Palomar 精选 AI 评分 95 ☆ Ralf Stephan 于 10 月 20 日发布新版本相关研究的 Hexagon 页面及 Palomar 形式化登记 PALOMAR-2026-10-20-000014，报告把 (3/2)^n 最近整数编码得到的 steering word T 的子词复杂度 p_T(k)/k→∞ 连同使用的 p-adic Subspace Theorem 全部形式化于 Lean 4。作者披露 Fable 5 探索新证明，Opus 4.8/5 协助 Lean 开发，数论专家 Yann Bugeaud 提供评论并建议简化，Fable 5.1 生成后续简化论证。该题材已有 arXiv:2607.11648 早期版本；10 月 20 日仅记录新增 Palomar/Lean 核验公开里程碑，不主张定理首次在当天提出，且未在本轮独立核验 kernel 运行。
形式化数学
推荐理由：结合具体专家反馈与大模型形式证明开发、并有当日新登记的内核审查证据，可作为历史既有论文的新可信度里程碑，而非重复计算首次发现。
08:00
P. M. Aronow & Patrick Lopatto / Hexagon 精选 AI 评分 95 ☆ P. M. Aronow 与 Patrick Lopatto 于 10 月 20 日发表低温 Sherrington–Kirkpatrick 自旋玻璃模型的 AI-assisted 研究：对来自 Gibbs 分布的典型起点，改进 Glauber 动力学总变差混合时间的概率上下界，报告 A_β n^{7/30}<log T≤n^{1−ω}（任意固定 0<ω<1/4）。研究声称扩展此前 OpenAI 的相关边界；GPT-6 Sol/Astra、GPT-6.1 Sol 与 Claude Opus 5.5 参与证明和复核。部分已知相关结论与五组指定结果拥有 Lean 4 形式化，但不能由此推出全篇所有分析步骤均已核验；提交者仅报告理解部分内容，尚未有独立审稿。
数学发现
推荐理由：对已公布的 AI 数学结果形成数学内容更强的独立研究路线，同时明确哪些子结论有机器形式化，是重要的 AI-assisted 数学物理进展样本。
08:00
Roelof van Dijk / Hexagon 精选 AI 评分 94 ☆ Roelof van Dijk 于 10 月 20 日在 Hexagon 首发稿件，声称对 OpenAI 的 Landau–Siegel 零点排除证明提出独立简化：通过 Frobenius 同余同时提供 determinant 整除和非零信息，利用截断下最大惰性素数上的多项式根计数取代较重的 resultant / Wronskian 步骤。作者披露新论证在与 GPT-6 Astra、Claude Opus 5.5 对话中发现，主张这些推导应归因于模型；Hexagon 标注 human understanding no parts，未附完整 Lean kernel 验证或独立专家审核。此项是更早公开零点结论的独立替代推导，而不是将最初结论重新日期。
数学发现
推荐理由：新证明组织方式直接回应数学家对 AI 数论论证可理解性与可简化性的要求，具有独立方法价值，且开放载明未获人工审阅的高风险限制。
08:00
Antti Hippeläinen / Hexagon 精选 AI 评分 94 ☆ Antti Hippeläinen 10 月 20 日发表由 Claude Opus 5.5 Agent 生成的数论证明主张：3-adic zeta value ζ₃(5) 无理。文章以 Hankel 行列式和 Volkenborn 积分研究 3-adic 分母与非消失性质，并给出一条依赖模曲线 X₀(3) 与过收敛模形式已发表结果的另一种论证；附公开的精确计算源码。作者明确说证明仅由其他 AI 实例互审，提交者阅读并核查文献但没有人类专家检验；无 Lean end-to-end 形式证明，因此不能称这项无理性结果已获得独立确认。
数学发现
推荐理由：重要 p-adic 数论新结论的纯 AI 证明主张具有可追踪双路径论证和计算附件，但仍明显低于专家审查或完整形式验证等级。
08:00
Antti Hippeläinen / Hexagon 精选 AI 评分 94 ☆ Antti Hippeläinen 于 10 月 20 日在 Hexagon 发布 Hodge 理论方向的 AI-generated 研究主张：对于 K=Q(√−3)、Hermitian signature (3,3)、判别式 −2 模范数的非分裂 Weil 型复阿贝尔六维簇，所有 Weil 类均为代数的。构造利用带 G₃₂ 反射群作用的 13 分支点曲线覆盖、Jacobian 成分、角色诱导关系和退化方法，并提供 GAP/Python 精确计算程序与球算术证书。作者披露证明、代码、文本由 Claude agents 生成，仅经过其他同类模型互审；有人类提交者核查参考资料，但没有人类数学专家审查、也未提供整体 Lean 核验证据。属于重大但尚待验证的 Hodge 相关研究主张，非已被认可解决的 Hodge 猜想。
数学发现
推荐理由：AI 自主研究触及特定高维阿贝尔簇 Weil/Hodge 类并公开可检查计算附件；选择性记录大胆主张及其严格的未审查边界，而非将其误报为经典大猜想获证。
10月19日 ⌄ 星期一 · 2 条
08:00
arXiv / SAIR Mathematics Distillation Challenge 精选 AI 评分 96 ☆ Georgios Kissas 于 2026 年 10 月 19 日在 arXiv 首次提交 Rózsa 论文，提出用于 SAIR Mathematics Distillation Challenge 第二阶段的 Python 等式推理求解器。任务在不预设结合律、交换律或其他代数性质的二元运算集合上，判断一条方程是否蕴含另一方程，并要求提供 Lean 可检查的证明或反例。Rózsa 通过逐步应用公理并维护推导证据搜索正向证明，同时搜索有限代数结构与一个固定无限模型以给出反例，统一导出 Lean 证书。作者报告官方主评测解出 199/200 题（99.5%），位列第六；对长链推导有效，但无限反例能力仍有限。论文结果为作者报告的挑战评测成绩，不等于 Radar 独立复跑或泛化至任意一阶代数问题。
定理证明
推荐理由：同日首次提交的原始论文给出高难代数等式蕴含求解器、可核验 Lean 证明与反例以及官方挑战成绩，使 proof-producing symbolic reasoning 的工程设计和评价具有清晰可审计性；明确区分证书验证能力和求解器的完备性。
08:00
Aran S. Ziegler / Zenodo 精选 AI 评分 92 ☆ Aran S. Ziegler 于 2026 年 10 月 19 日在 Zenodo 公开《Proof of the Arad–Herzog conjecture》的版本 3，声称完成 1985 年提出的有限非阿贝尔单群共轭类乘积猜想：两个非单位元共轭类的乘积至少包含两个共轭类。论文汇集已发表的交错群、特征标与有限 Lie 型群结果，并声称处理剩余情形及刻画奇维正交群中的特殊二类乘积。项目声明使用 OpenAI 与 Anthropic 的 agentic AI 工具推进研究策略、Lean 形式化与文稿。**这不是经过独立确认的猜想解决**：作者描述的 Lean 顶层结论是相对于大量文献分类与特征标假设的推导，依赖闭包含约 859 个公理/外部输入（其中约 269 项为具名非平凡数学假设），完整复核工件未公开；截至发布时没有独立专家审核。Zenodo 显示公开日期为 10 月 19 日，记录的更早技术创建时间不视为首次公开发表。
数学发现
推荐理由：1985 年以来的重要有限群论猜想出现具有明确 AI 角色披露的完整证明声称及可追踪存档；虽可能影响重大，但尚缺独立同行审查和不依赖外部数学公理的完整形式核验。按高重要性、低验证等级的未确认研究主张收录，而非宣告已证实。
10月18日 ⌄ 星期日 · 11 条
08:00
Thomas Hales / Hexagon 精选 AI 评分 97 ☆ Thomas Hales 于 10 月 18 日公开由 ChatGPT-6 Astra 在其提示下生成的研究稿：对 8、24 维 Cohn–Elkies 线性规划的径向 Schwartz 辅助函数，尝试以绝对可和系数上的无限线性方程组构造指定零点，经模曲线上的秩六全纯向量丛与 Riemann–Roch 证明归一化后的存在唯一性。文本明确承认所需的全局符号不等式没有从新系数方程独立导出，而是与 Viazovska 等已知 magic functions 认同后继承；因此这是一条新构造途径的未独立验证研究主张，不是重新独立证明球堆积极值。Hexagon 标注作者理解部分内容，正文由 Astra 生成。
数学发现
推荐理由：著名数学家提出有明确技术路线、可与经典球堆积证明比较的 AI-generated mathematics；所缺的关键符号约束也得到主动披露，便于后续同行核验。
08:00
Shawn Krisman / Hexagon / GitHub 精选 AI 评分 98 ☆ Shawn Krisman 于 10 月 18 日发布 Lean 4 / Mathlib 形式化成果，声称完整覆盖 Roy 的强六指数定理：对于两组分别在代数数域上线性无关的 2 个与 3 个复数，六个乘积中至少一个不属于由 1 和代数数对数张成的向量空间。证明链还形式化 Waldschmidt 的超越性定理及 Philippon 的重数估计，仓库公开 Lean 源码，报告仅使用 Lean 标准三条公理闭合。作者披露代码通过一次 Claude Code 会话、使用 Claude Opus 5.5 生成，Hexagon 标记 human understanding 为 no parts。本条是已有经典数学定理的新形式化，不是新发现该超越性定理；编译声明来自提交者，尚未由 Radar 独立复跑。
形式化数学
推荐理由：一次 AI-assisted Lean 形式化横跨高阶超越数论核心定理和复杂辅助理论，对数学形式化可扩展性极具指标意义；需严格区分公开 kernel-check claim 与第三方复现。
08:00
Deep Bhattacharjee & Ushashi Bhattacharya / Hexagon 精选 AI 评分 96 ☆ Deep Bhattacharjee、Ushashi Bhattacharya 于 10 月 18 日发表 AI-assisted 数学物理预印本：声称证明固定格距格点 Yang–Mills 在 |β|<1/(8d) 的唯一性和质量间隙，并把四维 SU(2) 单链 Dobrushin 方法阈值推进至 β_W<2/9。公开说明 Claude Code 协助证明、写作与 Lean 开发；Lean 4 的 25 个定理仅覆盖有限及代数步骤，Bessel 恒等式、调和延拓和 Riccati 比较等解析步骤保留在手写论证与数值检查中。作者明确声明连续 Yang–Mills 存在性与质量间隙问题仍开放，不可将格点模型的有限参数结果等同千年难题。
数学发现
推荐理由：具有明确的 PDE/数学物理适用范围、定量阈值及公开部分形式验证；避免把严格限定的 lattice 结果包装为 Clay 千禧年问题的解决。
08:00
Pedro Machado Manhães de Castro / Hexagon 精选 AI 评分 96 ☆ Pedro Machado Manhães de Castro 于 10 月 18 日公开组合学构造，报告否定 Barát–Gyárfás–Tóth 关于有序完全图多色无嵌套匹配阈值的猜想：对任意 r,k≥3，在经典单色 k-匹配的 Ramsey 阈值 (r−1)(k−1)+2k 个顶点上存在一种 r-边着色，使每个单色 k-匹配都含一对相互嵌套的边。证明使用端点计数和两次边重染色；研究者公开表示 ChatGPT、Codex、Claude 参与文献、构造与证明审查，自己理解并对数学内容负责。未报告 Lean kernel certificate 或外部独立同行评议。
数学发现
推荐理由：明确反驳已发表的组合猜想并给出适用于所有参数的构造，而且记录了多模型辅助、人类理解与缺乏独立验证的不同证据维度。
08:00
Qiyue Tang / Hexagon 精选 AI 评分 95 ☆ Qiyue Tang 于 10 月 18 日公布关于正对角可斜对称化整数矩阵的 Huang–Ma mutation invariant 研究，论文声称证明其二值猜想，确定每个矩阵尺寸允许的精确取值并给出实现相应取值的矩阵。作者在 provenance 中说明自己编写题目提示词，AI 约用 27 分钟生成完整解答，随后又借助 AI 审查与润色。Hexagon 标注人类理解部分内容，未提供 Lean 形式化或独立数学专家审稿；因此按作者公开的 proof claim 收录，而非将二值猜想表述为公认已解决。
数学发现
推荐理由：这是短时 AI 主导解决明确数学猜想的可追踪案例，关联 cluster algebra 与矩阵突变不变量；人工理解及证明验证阶段必须单独标注。
08:00
YURAN XIU / Hexagon / HAL 精选 AI 评分 95 ☆ YURAN XIU 于 10 月 18 日发布相互关联的两项图多项式构造（Hexagon 2610.00325v1 与 2610.00326v1），分别回答 Barton–Brown–Pike 的两个问题：一项构造 K46 与三个 P3 的 join，得到系数非单峰、但全部复根实部严格为负的 acyclic polynomial；另一项给出 230 顶点二部图，其 induced-forest 计数多项式在高次数区间先下降再上升。作者在两篇摘要中报告通过 Lean 验证图到多项式的恒等式、精确不等式及第一例中的有理 Lyapunov 稳定性证书。两项均标注 primarily AI-generated / human understanding no parts；为避免相邻同一主题重复灌水，以单个系列里程碑报道，关联论文 https://hexagonmath.org/2610.00326v1。
形式化数学
推荐理由：把同日两个互相关联、具有不同强度的反例纳入同一事件，保留有限可重算数学证书及 AI 生成但尚无人类理解的风险。
08:00
YURAN XIU / Hexagon / HAL 精选 AI 评分 95 ☆ YURAN XIU 于 10 月 18 日发表理论计算机科学 / 代数组合学新反例：对每个 n≥1，用 2n+1 个变量构造次数分别为 2、2、1 的三个实多项式，乘积在布尔立方体上处处为零、无共同布尔零点，但任何相应 Nullstellensatz 证书的特定多线性化分量次数至少 n+1。构造从 Kothari 等此前关于两多项式的障碍出发，引入 selector variable 把高次数障碍转移至三多项式乘积零设置。论文声称整个无界次数反例已在 Lean 4 核验，Hexagon 标注 primarily AI-generated、human understanding no parts；外部未独立复核。
形式化数学
推荐理由：对一个具有明确先行文献的算法代数推广给出全参数反例与形式证明主张，具有超出有限单个实例的理论价值。
08:00
YURAN XIU / Hexagon / HAL 精选 AI 评分 94 ☆ YURAN XIU 于 10 月 18 日公布对 Alekseev–Gaevoy 仿射子空间 union-stability 猜想的反例：在 F₂^N 中构造至多 2N² 个余维 log₂N 的仿射坐标子空间覆盖整个空间，但各子空间只删除约 1/N 的部分便导致其并集发生超出任何 N^{-c} 界的损失。利用 2k 个指定坐标与中间 Hamming 层，给出精确的组合计数，声称所有指数、任意大维数情形已通过 Lean 4 核验。该稿报告以 AI 生成为主、人类尚未理解，未经独立专家审查。
形式化数学
推荐理由：对复杂性理论中可明确定位的稳定性猜想给出具有全尺度强度的形式化反例，是可信证明产物与人类审查缺口并存的研究案例。
08:00
YURAN XIU / Hexagon / HAL 精选 AI 评分 92 ☆ YURAN XIU 于 10 月 18 日报告解决 Colmenarejo 等在 Stirling permutations/parking functions 中提出的 Problem 46 的三元素情形：对 {1,x,y} 给出基于奇偶性与 x+y≤2n 的充要分类，并推导包含 h=⌊(n−1)/2⌋ 的显式计数公式。作者在原始摘要中宣称分类、具体构造与计数均已通过 Lean 检查，并链接 HAL deposit。Hexagon 标为 primarily AI-generated、human understanding no parts；Radar 不宣称已独立编译或由外部专家审核。
形式化数学
推荐理由：有明确编号的开放组合学问题、一般参数结果及形式化声明，是 AI 生成组合证明的可定位小型案例；按精选门槛保留完整验证限制。
08:00
Ilya Sergey / VERSE Lab 精选 AI 评分 94 ☆ Ilya Sergey 于 10 月 18 日发表 Vermilion 实验项目说明，公开把 Verus 的 Rust 验证条件从 SST 转换为 Lean proof obligations 的新后端：Lean tactics 与重建后的 SMT 证明先自动处理简单义务，复杂证明可复用 Mathlib、由人类或编码 agent 交互完成。merge-sort 示例报告 40 个 obligations 中 31 个自动验证、9 个交互完成；一个小型对照 suite 中 Vermilion 相对原生 Verus 约慢 16 倍。作者披露最初原型在 GPT Astra、Claude Fable 帮助下实现。项目目前并非基础化的完整 Rust verifier：SST 到证明义务的翻译可信性、Rust 全语义、并发与不安全内存操作仍未形式证明或覆盖。
定理证明
推荐理由：它把 AI-assisted proof completion 与 Lean 数学库复用连接到实际程序验证，提供可检查的工具、测试及性能代价；其意义在于可扩展证明工作流而不是已经证明 Rust 前端完全正确。
08:00
Francesco Maggi / Terence Tao blog 精选 AI 评分 93 ☆ Francesco Maggi 于 10 月 18 日在 Terence Tao 博客发布八点评论，分析 LLM 数学证明与人类数学理解可能脱节的风险，讨论数学表述新概念（mathematization）、作者归属和同行评议、年轻研究者培养、未发表研究保密、私人前沿算力集中等问题。文章主张大学、专业学会、基金会协调建设具有自主治理与访问权限的科研 LLM 基础设施，并发展复现、贡献透明度及人才评估规范。它是作者的公共政策与学术生态建议，非已采纳的行业规范、成立的机构或新的实验研究结果；与 10 月 16 日 formalization library 路线及 17 日期刊筹备不是同一具体里程碑。
工具与生态
推荐理由：通过明确、可操作的研究资助与机构治理方案扩展 AI4Math 关于正确性之外的长期生态讨论；保留 opinion 与 enacted policy 之间界限。
10月17日 ⌄ 星期六 · 14 条
08:00
Terence Tao / Shaoming Guo 精选 AI 评分 94 ☆ Shaoming Guo 在陶哲轩博客发布联合筹备的新数学期刊设想：除开放获取外，拟优先奖励能加深数学理解的阐释，并要求拟录用论文的证明经过 Lean 形式化验证，以应对 LLM 时代大量难以人工逐一审查的证明。文章邀请社区讨论不同期刊的互补定位；截至本次公告，新刊仍在筹备，并非已经运行或正式采用的投稿政策。
工具与生态
推荐理由：它提出了清晰且可执行的 AI4Math 学术出版规则选择：formal verification 成为拟议的接收必要条件，同时评价重点从抢先发表转向深化理解；只记录筹备公告，不误报期刊已正式成立。
08:00
Carson Crocker / Hexagon 精选 AI 评分 98 ☆ Carson Crocker 在 Hexagon 报告二维 Euclidean Ramsey 问题 #188 的新界 7≤k≤60。下界由不可满足 SAT 实例与 DRAT 证书支撑，上界构造带 90 个正 24 边形的周期性红色区域，并用严格球算术验证任意 60 个连续单位间距共线点都触及红集。作者披露主要搜索、程序与文本由 Claude Code 在其指导下生成，两套上界检验程序采用不同方法；证书和代码开放，但没有数学专家完整审阅。
数学发现
推荐理由：它给出了显著的量化改进，并同时提供 DRAT、精确几何和两套区间算法形成可重算证据链，是 AI 生成数学与 computer-assisted verification 结合的鲜明实例；不将机器证书夸大为独立专家审稿。
08:00
Pappalettera & Sorella / Hexagon 精选 AI 评分 97 ☆ Umberto Pappalettera 与 Massimo Sorella 在 Hexagon 公开一份完全由 ChatGPT 6.1 Sol 生成的 PDE 研究手稿。手稿声称对任意有限 p>2，存在同一紧支撑零环量初始涡量，其无外力二维 Navier–Stokes 演化在黏性趋零时具有两个不同的强收敛子列极限；两者均为具有相同初始迹的重整化 Euler 解。贡献者明确不认领证明文本的作者身份，尚未理解与核验全文，正在组织 reading group 检查并解释该主张。
数学发现
推荐理由：若得到验证，将触及 PDE 中消失黏性选择机制的重要理论问题；目前价值在于公开高风险 AI-generated research claim 与明确安排人类核验，不能称为已获数学界确认的定理。
08:00
Manjul Bhargava / Hexagon 精选 AI 评分 96 ☆ Manjul Bhargava 在 Hexagon 发布后续论文：以 E:y²=x³−2x、P=(2,2) 为具体例子，声称存在正下密度的素数，使 P 模 p 的约化生成 E(F_p)，借用 Cureton–Thorner 的 Dedekind ζ 零点自由区域主张与 OpenAI 的 marked Type II 估计。作者用手写笔记制定策略，GPT-6 协助写作和细节；Lean 只形式化了在明列分析和算术前提下的一个主要推导，零点自由区域及若干基础引理仍作为假设，不能把整条无条件结论称作完整 kernel-checked 证明。
数学发现
推荐理由：这是 AI 数学成果与著名数学家主导的新论证相结合的跨论文结果，且将 Lean 形式化的边界明确限定为 conditional deduction，对科学归因和证明可信度均有代表性。
08:00
Pharos team / Hexagon 精选 AI 评分 95 ☆ Sun Zeming、Gao Guoxiong 与 Liu Shurui 在 Hexagon 发表代数几何研究，报告利用 Pharos 系统给出所有亏格及标记数下稳定曲线模空间第 15 上同调的表示分解重数公式，并声称在该情形证明广义 Hodge 猜想。披露说明 Pharos 负责主要数学研究与草稿，作者审阅了关键数学工具和证明路线，但未逐一核对组合分类和计算细节；未提供整项结果的独立专家核验或 Lean 形式证明。
数学发现
推荐理由：它体现专门 AI 数学研究系统参与高阶代数几何计算的潜力，并公开了人类已理解部分与仍未逐项核查的具体界限，适合以审慎的 research claim 方式记录。
08:00
Hexagon / Lean / GitHub 精选 AI 评分 97 ☆ Deep Bhattacharjee 与 Ushashi Bhattacharya 在 Hexagon 报告：维数 35 和 805 的半径 3 Lee 球均不能格铺砌 Z^n，填补 Xiao–Zhou 已覆盖规模范围内的剩余两例。论文披露主要证明、Lean 代码与多语言精确计算由人类在 Claude Code 中协作完成，给出 Mathlib 环境下不依赖 sorry、native_decide 或新增公理的 kernel-checked 结论，并提供 Zenodo 归档。该结果只证明 Golomb–Welch 猜想的 lattice form 中特定两例，不涉及任意非格铺砌，更未整体解决该猜想。
形式化数学
推荐理由：它将开放问题的具体剩余案例转成有明确形式化范围及机器检查记录的证据，是 AI-assisted discovery 与 trusted-kernel 形式核验结合的高价值样本。
08:00
Idris Ali Shaik / Hexagon / Palomar 精选 AI 评分 96 ☆ Idris Ali Shaik 于 10 月 17 日发表图的最大两个邻接特征值研究：论文报告一个普遍谱不等式、对一项精确 color-critical 界的无限图族反例，以及含最大度修正项的 F-free 图渐近最优界。三项主定理均由 Lean 4 形式化，分别有 10 月 15、16、17 日 Palomar 登记。作者使用 ChatGPT 与 Codex 辅助探索、形式化及文稿检查，并声明自己审阅 AI 产物且承担责任；登记日期不应被误当成三个独立的新论文发布。
形式化数学
推荐理由：同一研究把发现、构造反例和严格的定理加强与 Lean 证明产物连接起来，并有分项注册证据，值得作为单条完整论文里程碑收录而非拆分重复报道。
08:00
Kristoffer Josefsson / Hexagon / Palomar 精选 AI 评分 95 ☆ Kristoffer Josefsson 于 10 月 17 日公开论文，回应 Tabachnikov 问题：对所有 n≥4，循环排列的正数只要至少有两个局部极大与两个局部极小，就可表示为满足特定圆心角条件的凸多边形相邻三点外接圆半径；并讨论局部 C¹ 连续选取与全局障碍。论文声称存在性和连续性部分已在 Lean 4 / Mathlib 形式化，并对应 Palomar 2026-10-17-000001；披露列出 Claude Fable、Codex 的参与且作者声明理解全部内容。
形式化数学
推荐理由：提供可直接查阅的几何证明与形式化注册记录，反映 AI 工具与完整机器核验在精细几何定理中的协同，而不是仅靠公开摘要宣称成立。
08:00
YURAN XIU / Hexagon 精选 AI 评分 93 ☆ YURAN XIU 在 Hexagon 发布对有限域上 2×(k+1)×k、带分区形状零元约束的非退化超矩阵计数公式，报告证明 Koprowski–Lewis 的乘积猜想。方法把第一切片固定后的非退化性还原为偏线性映射的 simple-extension 条件，再逐层使用已有定理；作者报告完整计数结论及语义等价关系已在 Lean 中形式化，另有 HAL 登记。页面标为主要 AI 生成且人类尚不理解，不可升级为人类独立审稿。
形式化数学
推荐理由：其研究对象与计数公式明确，Lean 验证范围也具体，适合作为大模型生成组合学新证明并结合 kernel-checked 产物的样本，但需保持 statement fidelity 与独立审查的界限。
08:00
YURAN XIU / Hexagon 精选 AI 评分 94 ☆ YURAN XIU 在 Hexagon 首发论文，声称任意 q≥2 的 q 元 Hamming 立方体上次数至多 2 的布尔函数最多依赖 max{4,q+1} 个变量，并给出超过四变量时必存在 selector coordinate 的结构定理。作者说明两个结果均已用 Lean 4 / Mathlib 形式化且仅使用标准公理。页面披露主要 AI 生成、人类尚未理解全部证明；10 月 19 日另有 v2，10 月 17 日按首次公开 v1 收录。
形式化数学
推荐理由：给出精确组合结构界和可检查形式化结果，是理论计算机科学中具体、可复核的 AI-generated mathematics 证据；仅归因发布时的主张及 Lean 形式证明，不暗示独立人工审阅。
08:00
YURAN XIU / Hexagon 精选 AI 评分 94 ☆ YURAN XIU 在 Hexagon 发表此前 WADS 2023 所提 Set-Cover by Rotations 问题的复杂性结果：给定显式二进制模式与预算，判定若干循环移位能否覆盖全部位置是 NP-complete。文章通过 replicated-marker 和环图编码建立 3-SAT 的多项式归约，称 Lean 形式化涵盖数学归约、完整字串算法、NP membership 与无条件 NP-hardness 基础，并提供 HAL 归档。条目为主要 AI 生成，贡献者未声称已经完成人类数学审稿。
形式化数学
推荐理由：把具体公开算法问题从疑问推进为声称完全机器验证的复杂性分类，对 AI 驱动可验证理论计算机科学有明确价值；应将 kernel checking 与人类语义审核区分。
08:00
Nhat Minh Doan / Hexagon 精选 AI 评分 94 ☆ Nhat Minh Doan 于 10 月 17 日发布几何拓扑研究，声称对任意固定的一尖点或一条测地边界的双曲环面，长度不超过 L 的简单闭曲线中，不同长度数与等距轨道数相差 o(L²)；模环面特例与 Chen 于 10 月 16 日的 Markoff 数密度唯一性结论对应。论文还提出特定曲面的 Schmutz–Schaller 重数界。作者披露 Astra、Sol 与 Codex 参与证明推导和文稿检查，尚未独立验证每段生成论证，也没有 Lean 证明；这是基于前日工作的实质性推广，而非前日论文的转载。
数学发现
推荐理由：相较前日已收录的 Markoff 结论，本稿把对象拓展到更广泛的双曲几何长度谱，并公开 AI 深度参与与未审核状态，符合有新增数学范围的 follow-up 里程碑标准。
08:00
Boon Suan Ho / Hexagon 精选 AI 评分 94 ☆ Boon Suan Ho 在 Hexagon 发表 AI 深度参与的图标号研究，从同一个生成函数恒等式发展模单位根剩余类、单位圆正性 / Goemans–Williamson 最大割半定规划，以及稠密子图标签跨度三类非 graceful 证明工具。文章据此提出 Paley、Kneser、edge-transitive 与高阶正则图等新排除家族，并分析正性方法的能力边界。作者披露 Claude Opus 5.5 执行论文写作、探索和精确计算，GPT-6 Pro 参与部分结果；作者未逐条审阅全部证明，也不把模型间互审当作外部专家评审。
数学发现
推荐理由：该事件重点是能重复使用的数学阻碍方法，而不只是个别图实例，并有细致的 AI/人类角色披露，为 AI 生成数学方法及其核验需求提供有信息量的案例。
08:00
Sebastien Palcoux / Hexagon 精选 AI 评分 92 ☆ Sebastien Palcoux 于 10 月 17 日公开 AI 辅助的复融合范畴 Grothendieck 环分类研究：报告秩 2–4 的一般分类以及秩 5–8 在明确融合重数约束下的分类结果，并发布精确 fusion-ring census、验证代码、交互 atlas 及七个潜在新张量范畴构造。作者明确保留两项秩 6 categorification 开放问题；项目材料主要由 AI 生成，既无独立专家复核，也未完成 Lean 形式化，七项构造的新颖性仍待核验。
数学发现
推荐理由：除论文主张外还提供结构化枚举和交互查询基础设施，展示人类主导的 AI 数学分类工作流；通过保留开放问题与验证缺口，避免把未经确认的候选构造当作成熟定理。
10月16日 ⌄ 星期五 · 6 条
12:23
Hexagon / GitHub 精选 AI 评分 97 ☆ Shawn Krisman 于 10 月 16 日公开一项 primarily AI-generated 数论结果及完整 Lean 4 certificate：Dirichlet beta function 的 17 个偶数值 β(4),β(6),…,β(36) 中至少一个是无理数。与已有显式结果常包含 Catalan 常数 β(2) 不同，新结论完全排除 β(2)。证明沿 Ball–Rivoal / Rivoal–Zudilin 路线构造二阶导数线性形式，通过 p-adic denominator analysis、精确有理证书、实轴 size bound 与 saddle-point nonvanishing 完成；仓库包含 62,131 个 event intervals 等数值证书，全部在 Lean kernel 中检查。项目由两次 Claude Opus 5.5 sessions 主导产生，仓库于 10 月 16 日创建；作者明确说明尚无人类专家审阅数学或 Lean 代码。
数学发现
推荐理由：这是 AI-generated research mathematics 与强 formal evidence 结合得非常完整的案例：结论具有明确的新数论增量，且从解析估计、p-adic 计算到数值 certificate 全部落入 Lean kernel proof。其主要剩余风险是 statement / mathematical interpretation 尚无人类专家独立审阅，而不是 proof hole。
08:00
Terence Tao / SAIR 精选 AI 评分 96 ☆ Terence Tao 于 10 月 16 日宣布 SAIR Open Math OS 软启动。当前服务托管 DeepSeek V4.1 Flash、Kimi K3 与 GLM 5.3 Flash 等开放数学模型，能力约落后 frontier models 一年左右，但已可承担中等规模 Lean formalization、数学论证总结与讨论等任务。平台强调 team accounts：团队成员可共享彼此的 prompts，以适配协作研究；算力来自捐赠，并正向学术机构申请者提供免费账号。SAIR 同时继续招募合作方，计划在开放基座模型上进行数学专用 post-training。它把 9 月 18 日的 Open Math Model initiative 从倡议推进到可实际使用的开放服务。
工具与生态
推荐理由：这是开放 AI4Math 基础设施从愿景进入可运行阶段的明确 milestone：不仅提供开放模型访问，还把团队协作、学术免费账号、捐赠算力和未来数学 post-training 组织到同一平台。它与 9 月的 initiative 公告不同，新增的是实际 soft launch 与服务形态。
08:00
Xena / Lean community 精选 AI 评分 96 ☆ Jeremy Avigad、Kevin Buzzard、Johan Commelin、Rémy Degenne、Kim Morrison、Oliver Nash 与 Adam Topaz 于 10 月 16 日发表共同文章，回应 AI 快速 autoformalization 后“尽快形式化全部数学”的呼声。作者支持大规模形式化目标，但强调形式 artifact 的价值不仅是 correctness，还在于能否被数学家理解、维护、重构和继续用于新研究；以 AI sphere-packing code、Anthropic 1300 万行 FLT formalization 和 OpenAI 数学发布为案例，警告低质量一次性代码可能浪费资源并破坏社区激励。文章提出以 Mathlib、Formal Conjectures、AnnalsChallenge、Tau Ceti、Formal Frontier 与 Palomar 等互补机制为基础，由数学家控制 roadmaps、library design、hosting 与治理。
工具与生态
推荐理由：这是来自 Lean/Mathlib 核心研究者的一份实质性社区路线图：把 AI formalization 的评价标准从“能否生成 kernel-accepted code”提升到可复用性、设计一致性、语义质量、治理和长期数学价值，对未来大规模 AI-generated formal libraries 的资源配置与质量门槛有直接影响。
08:00
William Y. Chen 于 10 月 16 日在 Hexagon 发布结果：Frobenius 1913 年猜想断言每个 Markoff number 都由唯一的有序 Markoff triple 产生；新工作证明至少其 density-one 版本成立，即 X 以下 Markoff 数中的非唯一例外比例趋于 0。证明把同一 Markoff 数对应到 modular torus 上等长简单闭测地线，再用 McShane–Rivin stable norm、rational linear symmetries 与 Markoff surface 上 mapping class group 的 3-adic analytic dynamics，把非对称重复表示压到密度零。Chen 明确披露项目主要通过 ChatGPT Astra / Codex 与 Claude Fable 5.1 完成：作者给出初始想法并指导研究，但成稿中的主要论证 largely due to Astra。当前 Hexagon 标注 human understanding 为 some parts，未提供 Lean certificate 或独立专家审稿。
数学发现
推荐理由：这是一个百余年经典唯一性猜想的实质性 density-one 进展，而且作者将主要 proof development 明确归因给 frontier agents。Radar 同时保留证据边界：这是作者发布的 AI-generated research claim，尚无形式化 proof 或独立专家验证。
08:00
Thomas Hales / Hexagon 精选 AI 评分 93 ☆ Thomas Hales 于 10 月 16 日提交由 GPT-6 Astra 在其 prompting 下生成的《Linchpin Theorems》。核心观点是：proof assistant 只能确认形式 proposition 被证明，不能确认这个 proposition 就是人类真正想表达的数学；当 AI 批量 autoformalize 大型理论时，应挑选一组意义可由较少基础设施人工审计、但其 formal proofs 又连接到大规模下游结果的“linchpin theorems”。文章用 sphere packing、Lie algebra classification、regularity theory、Weil conjectures 与 complexity 等案例说明这种 semantic anchoring 思路。Hexagon provenance 明确标注文本由 ChatGPT-6 Astra 生成、没有人类 authorship，Hales 作为 contributor 提出任务与发布结果。
评测与数据
推荐理由：它把 Hales 此前关于 kernel correctness 与 statement fidelity 的一般风险，进一步变成可操作的 library-audit 设计：无需人工重读每一行 AI-generated proof，也能通过少量高语义价值锚点检查大规模 formal development 是否仍对应预期数学。对未来百万到千万行自动形式化库尤其直接。
01:55
arXiv / GitHub 精选 AI 评分 92 ☆ Xu 等提出 LeanGraphSearch：先从 Mathlib 的 forward dependencies 构建 declaration graph，再从语义检索得到的初始候选向其多跳依赖传播 relevance，最后重新排序供 prover 使用。论文在 MathlibQR 上报告相对最强 baseline LeanSearch v2 的 recall 最高提升 12%，在 MathlibMPR 上完整覆盖 annotated proof-route groups 的比例额外提升 3.7 个百分点；将检索器接入带 Lean feedback 的迭代 proving loop 后，在 8/16/32 轮 reflection 设置中，pass rate 相对原始 prover 最高提升 40%，相对 LeanSearch v2 最高提升 10%。公开仓库提供统一检索/证明实现、benchmark 子集和复现实验说明。
定理证明
推荐理由：它把 premise retrieval 从相似度搜索推进到显式利用 formal library 的证明依赖结构，并证明这种结构化检索不仅改善 retrieval 指标，还能传导到端到端 Lean proving。对大型 formal libraries 中的可扩展 theorem-proving agent，这是比单纯扩大 embedding model 更有结构信息的方法。
10月15日 ⌄ 星期四 · 7 条
21:46
Milikic、Bamas、Abbe 与 Kunčak 训练可在 GPU 上批量预测 Lean acceptance 的 neural evaluators，以缓解 RL / search 中频繁调用 Lean verifier 的吞吐瓶颈。训练集包含约 484 万个 Lean-labelled programs；两阶段 evaluator 在 68,932 个公开 prover 生成程序上达到 87.8% acceptance-prediction accuracy，并在单张 H100 上达到约 3.5 candidates/s，论文称相对具有 environment reuse 的 64-worker Lean baseline 吞吐提高 4.2 倍。将 learned feedback 与真实 Lean reward 混合用于 GRPO 后，训练 wall-clock 约降低 31%；一轮训练后的 miniF2F pass@1 与 Lean-only reward 基本持平，pass@32 略高。作者仍把 Lean verifier 保留在 hybrid loop 中，learned evaluator 是加速代理而非 trusted kernel 替代品。
评测与数据
推荐理由：它直击 formal RL 的系统瓶颈：kernel verification 精确但昂贵，而 GPU proxy 可以承担大规模候选预筛与 dense feedback；关键是论文没有把 learned verifier 冒充可信证明器，而是在 hybrid protocol 中保留 Lean 作为最终 ground truth。
08:00
Simons Foundation 精选 AI 评分 96 ☆ Simons Foundation 于 10 月 15 日宣布与 Anthropic、OpenAI 共同投入总计 1500 万美元的资金与资源，支持数学共同体系统应对快速增长的 AI-assisted research。计划由 Simons Foundation 管理并通过开放征集资助 workshops 与 community initiatives，重点包括独立评估 AI 产生或辅助的数学结果、帮助数学家掌握相关工具、讨论科研规范与职业影响，并让数学界参与塑造 AI 在本领域的使用标准。OpenAI 同日说明将贡献 500 万美元，并提供模型与计算访问；产业方提供资源，但资助流程由基金会面向数学共同体组织。
工具与生态
推荐理由：这是 AI4Math 从模型能力竞争进入社区验证与制度建设的高信号事件：第三方数学基金会获得独立组织权，把结果复核、工具培训、科研规范和数学家参与治理变成专门资助对象，而不是由模型公司单方面定义评价标准。
08:00
Leonardo de Moura / Lean FRO 精选 AI 评分 96 ☆ Leonardo de Moura 于 10 月 15 日系统说明 Lean 在 AI-generated formal mathematics 激增后的新信任架构。Lean v4.35.0 实际已于 10 月 12 日发布，其中 `lake check` 可调用随发行版提供的多个独立 checker，`--paranoid` 会同时运行 hardened official kernel 与 lean4lean、NanoDa、con-leche、con-ron 等外部实现。10 月 15 日文章重点披露其 AI provenance：con-leche 是用 Lean 编写并带一致性证明的 kernel，由 Claude Fable / Opus 在 Joachim Breitner 高强度监督下实现和证明；con-ron 则从 con-leche AI-assisted 翻译到 Rust，并用 Aeneas 建立 refinement 关系。de Moura 强调多实现、跨语言/运行时检查可降低单一 kernel、编译器或 runtime 的共同失效风险。
工具与生态
推荐理由：这不是把 10 月 12 日的 Lean v4.35 release 重新定日，而是官方首次集中披露 AI-built verified kernels 的生产方式与推荐 trust model。随着 AI 自动生成海量 Lean proof，可信性从“一个 kernel 接受”升级为多实现、跨 runtime、形式 refinement 的防御纵深，对整个 AI4Math verification stack 都有直接影响。
08:00
Palomar / GitHub 精选 AI 评分 93 ☆ JD Jones 的 AI-assisted probability project 于 10 月 15 日进入 Palomar。结果主张：对关于 0 对称、且几乎处处满足 0<a≤|X|≤b 的实随机变量，只要 b/a≤√3+√2，就有 E exp(tX)≤exp(t²E[X²]/2) 对所有实 t 成立，且非零 t 时严格；实际方差是最优 quadratic proxy，而任何更大的 universal support ratio 都存在显式四点反例。开发还给出 sharp eighth-order MGF gap、critical-law rigidity 与 squared-law Wasserstein stability。公开 disclosure 说明问题提案、proof development、exact certificates 与 formalization 大量由 GPT-6 Astra / GPT-6 Pro / Codex agents 辅助或生成，没有人类 specialist review。Palomar 对固定提交进行 statement comparison，并用 Lean kernel、NanoDa 与 con-ron 重放；因此 10 月 15 日记录的是独立 registry / multi-kernel verification milestone，而非把更早公开的数学结果重新定日。
形式化数学
推荐理由：底层项目在 10 月 10 日已经公开、10 月 14 日已有 exact-commit Linux gate，因此本条只记录 10 月 15 日新增的独立 registry preservation、statement comparison 与多 kernel replay。它也是 AI-generated / AI-reviewed 新数学如何逐层增加外部可审计证据的代表案例，同时仍明确没有人类专家审稿。
06:21
Axiom Math / Hexagon 精选 AI 评分 95 ☆ Kenny Lau / Axiom Math 的 CollatzPositiveDensity 项目在 10 月 14 日形成新的强化里程碑：22:21 UTC 的提交把显式常数优化到 87640，并扩展 even target 情形；随后补齐 formalization metadata，同日 Hexagon 发布论文。写 L=2^(2^(2^87640))，则对所有 X≥2^L，至少 X/L 个正整数 n<X 在 floor(10.46 log n) 次 ordinary Collatz steps 内到达 1；项目还给出 odd-starting / accelerated-step 版本，以及对任意 3∤t 的 prescribed-target 正密度结论。作者说明研究目标由人提出，而 AxiomProver 自主产生数学推导并生成 Lean formalization；Challenge 只依赖 Mathlib，Comparator 检查四个主结果，formalization metadata 记录无 sorry 且仅使用 Lean 三个标准公理。
数学发现
推荐理由：仓库本身在 10 月 9 日已公开，因此本条不把项目重新定日；收录的是 10 月 14 日可由不可变 Git commit 固定的实质强化：显式常数优化、target 范围扩展与完整研究稿件发布。它展示了 human-directed、AxiomProver-autonomous 的数学改进如何直接进入可比较的 Lean certificate。
00:43
Plasma AI · GitHub 精选 AI 评分 98 ☆ Plasma AI 于 10 月 14 日公开 Erdős Problem 408 的新解：设 f(n) 为反复应用 Euler φ 函数到 1 所需的最小次数，则存在 α∈[1/log 3,1/log 2]，使 ∑_{n≤x}(f(n)−α log n)^2 ≪ x(log x)^2/(log log x)^5；因此 f(n)/log n 在自然密度 1 的集合上趋于 α，回答该问题关于 distribution function 与 almost-always constancy 的前两问。结果把 1990 年 Erdős–Granville–Pomerance–Spiro 在 Elliott–Halberstam 型假设下的正规阶结论变为无条件结果，关键输入来自 OpenAI 的 7/8 zero-free half-plane 与 shifted-prime / weighted-dilation-graph machinery。项目同日公开 Lean 4 development：Challenge 复用 formal-conjectures 的问题陈述，Solution 证明三个 comparison targets；formalization.yaml 记录 Claude Opus 5.5 / Claude Code 与并行 subagents 参与形式化开发，但目前数学论证仍是 self-assessed，未记录独立专家审查。
数学发现
推荐理由：这是明确的新研究数学结果：把一个经典 Erdős 问题的前两问从条件结果推进到无条件正规阶，并同时公开长篇 Lean certificate。AI 的作用不是边缘润色，而是项目本身以 Plasma AI 为作者、并用 agentic formalization 把新论证连接到 OpenAI 等近期 AI 数学基础资产。
00:29
He 等提出 IneqAgent，把 LLM 推理与精确 symbolic computation 组合成 Lean 4 inequality prover：lemma-level Monte Carlo Tree Search 协调 lemma construction、goal reformulation 与 backend selection，sum-of-squares、Bernstein 与 successive difference-substitution 等后端生成局部精确证书，再由 LLM 与 Lean feedback 组装完整证明。论文报告 DeepSeek-V4-Flash 配置在四个 benchmark 上解出 175/186（94.09%），并在四种 backbone 上相较相同模型的 Direct Agent 呈现更好的低推理成本 success-rate。除 benchmark 外，系统还得到并 Lean 验证 Dittert conjecture 在维数 4、5 的 strengthenings，并认证 Holens–Djokovic (4,4) inequality，从而推出四维 Merris conjecture。
定理证明
推荐理由：它不是单纯增加 sampling 的 prover，而是把可验证的符号计算后端变成 agent search 中的一等动作，使 LLM 负责结构推理、专用算法负责 exact certificate，并用 Lean 将二者闭环；同时出现了 benchmark 之外的新数学 strengthening。
10月14日 ⌄ 星期三 · 3 条
17:27
Chen 等提出 Euler，一个面向长期数学研究的 human-centered multi-agent system。与只输出最终答案的 agent pipeline 不同，Euler 把数学陈述、assumptions、proof dependencies、alternative approaches、failed attempts 与 verification evidence 组织成共享 research graph；agent 跨 session 读取持久化、任务相关的图结构，人类可以回到任意 graph node 及其保存的 team state，检查早期推理并从该节点探索替代路线。论文以三个数学研究 case studies 展示系统，并把 Lean kernel checking 纳入 evidence levels。其核心贡献是把长程数学探索的 provenance、失败记忆与 human steering 变成系统级对象，而不是只保存最终 proof transcript。
工具与生态
推荐理由：长期 agentic mathematics 的关键难点并不只是单题成功率，而是 unsupported claims、上下文碎片化、失败路线丢失和人类难以介入。Euler 把这些问题统一到可追踪 research graph 与 persistent team state 中，对可审计、可继续的人机数学研究工作流具有方法学价值。
10:51
van Doorn、Monticone 与 Nathanson 于 10 月 14 日发布三元素 h-bases 的正负性分类：若允许集合 A 含负整数，则对 k=2，最大覆盖区间 n_h^flat(2) 在 h 为奇数或 h=4 时严格小于经典非负值 n_h(2)，而在偶数 h≠4 时两者相等。论文明确说明，这些 comparison results 的原始证明由 Harmonic 的 formal reasoning agent Aristotle 自主发现并在 Lean 中形式验证；论文作者随后给出新的、人类可读证明，并注明 Aristotle 的原始解使该工作成为可能。该事件因此同时具备 autonomous discovery、formal verification 与 human reconstruction 三层证据。
数学发现
推荐理由：它提供了一个证据链异常清晰的 autonomous AI mathematics 案例：agent 先独立发现并形式验证分类定理，随后人类数学家重构出新的传统证明。相比只给 machine-checkable artifact，这种 human reconstruction 显著提高了结果的可理解性与可审计性。
05:42
Pan、Szegedy 等于 10 月 13 日提出 definition grounding：不再只判断 AI 生成的 Lean definition 是否能编译，而是用后续 layered statements 持续测试该定义是否足够一般、idiomatic 且可复用，并据此迭代修订。ReuseBench 实验显示，LLM 从 textbook text 形式化的一组 definitions 中，只有约 25%–50% 能与全部后续 statements 兼容；澄清 informal definitions 后，跨模型平均兼容率最高可到 77.5%。作者还发现，只陈述少量 basic properties、暂不要求证明，就能以约完整 definition-formalization 11% 的成本显著增强 model judges 对 compatibility defects 的检测。
评测与数据
推荐理由：这项工作把 autoformalization 的质量标准从“局部 code typechecks”推进到“定义能否支撑后续数学”。对大规模 AI-generated libraries，这是比单题 proof success 更关键的长期可复用性指标，也与 Radar 一直强调的 statement / semantic fidelity 风险直接相连。
10月13日 ⌄ 星期二 · 4 条
20:48
arXiv / LeanEval 精选 AI 评分 94 ☆ Browning 等于 10 月 13 日发布 AnnalsChallenge 论文：从 2020 年以来《Annals of Mathematics》的 207 篇论文中筛选并手工形式化 50 个 main theorem statements，建立在 Lean 4 / Mathlib 上；每个 statement 都经过人工 review，并再次用 AI audit，必要时还咨询原论文作者。论文不提供 gold proofs，而是把这些可信 research-level statements 作为 proving benchmark。作者报告截至 10 月 2 日的社区 LeanEval submissions 中已有 40/50 获 accepted proof，其中 Axiom Prover 覆盖全部 40；同时指出大量 differential / Riemannian geometry、Shimura varieties 等论文仍因 Mathlib 基础设施缺失而难以仅陈述主定理。
评测与数据
推荐理由：它把 ATP / autoformalization evaluation 从竞赛题和本科数学推进到近年顶级研究论文的主定理，并用人工 formalization + human review + AI audit 优先保障 statement trustworthiness。更重要的是，它暴露了研究级 formalization 的真正瓶颈往往不是证明搜索，而是 formal library 能否表达该领域。
17:09
Axiom Math · GitHub 精选 AI 评分 97 ☆ Axiom Math 的 DedekindZetaZeroFree 仓库在 10 月 13 日 09:09 UTC 提交 `improve zero-free bound to 31/32`，把前一日公开的 Re(s)>1−1/6000 强化为：对任意 number field K，Dedekind zeta function ζ_K(s) 在 Re(s)>31/32 中无零点；10:10 UTC 又加入 finite-order Hecke character 的同半平面 corollary。Dean Cureton 与 Jesse Thorner 负责研究方向与数学判断，AxiomProver 生成证明和 Lean formalization。形式化的 Challenge 接口只导入 Mathlib，但完整 proof development 还依赖 Tau Ceti、vendored FiniteAbelianGlobalReciprocityv2，并适配了 LeanPool / openai-math 的材料；最终主结果的 proof dependency audit 仅出现 propext、Quot.sound、Classical.choice。
数学发现
推荐理由：这是前一日 human-directed / AI-generated 数论工作的实质强化，而非单纯修订措辞：zero-free boundary 从 5999/6000 显著推进到 31/32，并在同日上午扩展到 finite-order Hecke L-functions。Git 历史把强化发生时间和 formal artifact 的演化清楚固定下来。
08:00
Boyang Hu 于 10 月 13 日在 Hexagon 发布一篇 primarily AI-generated 数论稿件：对任意 number field F 和 global Weil group W_F 的任意有限维连续 unitary representation r，主张 L_F(s,r) 在 Re(s)>7/8 无零点，并刻画该半平面中的可能极点。解析核心先把 OpenAI quasi-Riemann 的 cubic-theta 方法从 Q(√−3) 上的有限阶 Hecke characters 推广到任意 number field、包括 nontrivial infinity type 的 unitary Hecke characters，再用 Brauer induction 与 Frobenius reciprocity 提升到有限维 Weil representations。作者披露 10 月 7–13 日由 GPT-6 Pro 主导多轮推广与重写，Claude Opus 5.5 参与最后 exposition / citation audit；当前完整证明尚未获人类独立验证，Lean formalization 仍在开发。
数学发现
推荐理由：它是 OpenAI quasi-Riemann 路线向更广泛 automorphic / representation-theoretic 对象的明确 AI-generated research extension，并给出可产生 Artin L-functions、Chebotarev、weight-one forms 与 CM motives 等后果的统一框架；但由于尚无人类独立核验和完成 Lean certificate，Radar 明确保留较低证据等级。
03:40
arXiv / GitHub 精选 AI 评分 93 ☆ Ortega 等提出 mini-Lean-agent：把 formal theorem proving agent 压缩成一个通用 coding-agent loop，模型可见工具只有 bash；模型自己读写仓库、搜索本地 Lean library、调用 Lean 并管理中间状态，最终结果则由独立 trusted evaluator 使用 Lean FRO Comparator 验证。论文在 Putnam 2025 的 12 道题上比较 minimal harness 与 AxProverBase / Numina-Lean-Agent：Gemini 3.8 Flash 在每题 2 美元限制下用 mini-Lean-agent 解出 7/12，而 AxProverBase 解出 4/12；使用 Astra 时 mini-Lean-agent 达到 12/12，平均成本 1.28 美元/题。作者主张以后评测 theorem-proving infrastructure 应至少与这种极简通用 coding-agent baseline 比较，以区分 base-model 能力和 specialized harness 的真实增益。
评测与数据
推荐理由：它提出了一个重要的 evaluation control：如果通用 coding agent + bash + compiler feedback 已经能达到甚至超过复杂专用 prover harness，那么 benchmark 增益不能再默认归因于专用 theorem-proving infrastructure。这个 baseline 直接影响未来 ATP agent 的 ablation、成本比较与系统设计。
10月11日 ⌄ 星期日 · 4 条
17:35
William D. Banks 于 10 月 11 日发布对 OpenAI Landau–Siegel-zero 证明的独立数学重构：保留原 AI 稿件的 interpolation-determinant 核心思想，但把论证整理为直接证明并给出显式常数。对 primitive real Dirichlet character，先得到 q₀=10¹⁰、δ₀=3.0×10⁻³；再结合 Lu–Zaman–Zhao 的有限范围计算，把结论扩展到所有 conductor q≥3。Banks 明确说明 underlying ideas 来自 OpenAI manuscript，而 explicit constants 与 presentation 是新的。该工作把一次大模型提出的高影响数论论证推进到人类专家可逐步审阅、可比较具体常数的形式，但当前仍是 preprint，并不等于社区已完成独立同行评审。
数学发现
推荐理由：这是对 frontier-model research mathematics 最有价值的一类 follow-up：人类专家没有只是转述 AI 结论，而是重新组织证明、显式化常数并接上已有计算结果，使 AI 生成的突破性 claim 更接近传统数学可检查、可引用、可继续改进的研究对象。
08:00
Palomar / GitHub 精选 AI 评分 94 ☆ Mark Lewko 的项目证明 Riemann zeta 零点计数的统一估计 N(σ,T)≤Cε T^((39/17)(1−σ)+ε)，其中常数先于 σ、T 选择；同时给出更精细的 piecewise density curve，在 σ∈[1/2,1] 上的 coefficient envelope 最大值为 39/17，相比 Guth–Maynard 的 30/13 coefficient 更小。项目还形式化一个 middle-range large-values estimate。公开 metadata 披露 formalization 与 release preparation 使用 AI assistance，并有独立 AI-assisted internal review。Palomar 于 10 月 11 日注册该结果，Comparator 将 Mathlib-only Challenge 与 Solution 对照，并由 Lean kernel、NanoDa、con-ron 检查；自动审阅同时指出 provenance metadata 应补列 Guth–Maynard 论文，因此没有把 registry acceptance 表述成人类 peer review 或 novelty certificate。
形式化数学
推荐理由：它把 analytic number theory 中非平凡的 zero-density / large-values 结果推进到可重放的 Lean proof surface，并同时公开常数依赖与边界处的不统一性。相比单纯形式化既有定理，它还包含更强 bound 的研究增量；Palomar 的多内核检查和审阅意见又把验证强度与 provenance 缺口同时显式化。
08:00
Palomar / GitHub 精选 AI 评分 96 ☆ Scott Armstrong 与 Amélie Loher 公开并注册对 Kupiainen–Rhodes–Vargas 2020 年 DOZZ theorem 的 Lean 4 / Mathlib 形式化。项目不仅覆盖 Liouville CFT 三点 structure constants 等于 DOZZ formula，还形式化 reflection coefficient、Gaussian multiplicative chaos、BPZ equations、analytic continuation、fusion asymptotics、shift equations 等主要 prerequisites，并记录原论文中的 errata 与 Lean statement deviations。仓库明确说明 Lean 代码由 AI coding agents 在作者监督下编写，作者在 proof development 前逐一定稿 exact definitions 与 theorem statements。Palomar 于 10 月 11 日用 Mathlib-only Challenge、Lean kernel、NanoDa 与 con-ron 检查核心声明，并将自动 statement review 与人类同行评审严格区分。
形式化数学
推荐理由：这是 AI-assisted formal mathematics 从单个 research theorem 向完整高复杂度概率/数学物理证明链扩展的强案例：不仅主定理进入 Lean，关键概率论、特殊函数与 CFT prerequisites 也被纳入同一可审计 development，并由作者显式掌控 statement fidelity。
08:00
10 月 11 日，丘成桐数学与人工智能实验室联盟在清华大学求真书院挂牌成立，由清华大学求真书院、丘成桐数学科学中心、北京雁栖湖应用数学研究院、中科院晨兴数学中心、上海数学与交叉学科研究院、东南大学丘成桐中心、河套数学与交叉学科研究院（深圳）和香港中文大学致真交叉数学科学院等八家机构组成。官方信息称联盟将汇聚近千名数学人才与科研团队，重点自主研发数学科学专用模型，并共享大模型训练资源、形式化数学库与算力平台，同时推进 AI 辅助形式化证明、猜测发现、可解释 AI 和交叉领域智能计算。
工具与生态
推荐理由：这是机构级 AI4Math 基础设施与人才网络的明确扩张：不是一次泛化的 AI 合作倡议，而是八家一线数学机构围绕数学专用模型、formalized mathematics libraries、训练算力与研究流程建立长期联盟，潜在影响覆盖中国 AI4Math 的模型、数据、验证与人才供给。
10月10日 ⌄ 星期六 · 4 条
22:47
Hexagon / GitHub 精选 AI 评分 91 ☆ Qiyue Tang 在基于 OpenAI Result 198 的 refinement 工作中，把 infinite little finitistic dimension 的构造简化并扩展到 every field；10 月 10 日进一步公开 Note198-formalization。项目固定 Lean 4.34.1 / Mathlib 依赖，对列出的 58 个 targets 运行 28 个 Comparator groups，接受目标的依赖只出现 propext、Classical.choice、Quot.sound 且无 sorryAx，并保存 verification logs / receipts。上游研究过程披露先由 GPT-6 Astra Pro 做 adversarial review 与 strengthening，再由独立 GPT-6 Astra 再审；Lean 仓库则明确说明 AI 用于形式化准备与 proof review。项目同时说明 formalization 覆盖的是列出的目标，不声称逐句覆盖整篇 manuscript，也不把机器 verification 等同于 human verification。
形式化数学
推荐理由：它展示了对一次 frontier-model algebra result 的外部 human+AI refinement 如何继续进入可重放的 Lean / Comparator 审计链。价值主要在独立 formal verification 与 dependency pinning，而不是把原 OpenAI Result 198 再记一次。
20:35
Kenta Kitamura · GitHub 精选 AI 评分 94 ☆ Kenta Kitamura 于 10 月 10 日新建公开仓库，在 OpenAI 已解决的 Gaussian moat / uniform Gaussian moat 之上提出并证明两个更强结论：对任意不可约齐次二元整系数形式 F（次数至少 2），具有有界素因子数的格点集合在任意固定步长图中具有统一有限 component bound；进一步，对任意非零齐次二元形式，存在任意长 bounded-step few-prime-factor walks 当且仅当 F 是常数乘某个整系数线性形式的正整数次幂。项目给出 Formal Conjectures 风格 statement、完整 Lean 4 proofs、axiom audit，并于当天在公开 Lean4Web 上重新检查三个目标；作者明确披露 ChatGPT 与 OpenAI Codex（GPT-6 Astra、GPT-6.1 Sol）参与数学探索、proof development、formalization 与文档。
数学发现
推荐理由：这不是对 OpenAI Gaussian-moat 结果的重复形式化，而是把结论推广到一个更宽的 binary-form / few-prime-factor 分类定理，并提供完整 Lean proof artifacts。AI 的角色也明确覆盖数学探索与证明开发，而不只是润色或机械翻译。
08:00
MathOverflow / Palomar / GitHub 精选 AI 评分 95 ☆ Eric Naslund 在 10 月 10 日公开更新 planar unit-distance exponent：新的 computer-assisted construction 给出约 1.043171 的下界，较此前 1.04273 进一步提升。工作由 Claude、Muse 与 Codex 辅助修改与搜索，并保留超过 10 万行 Lean 形式化。Palomar 同日注册 PALOMAR-2026-10-01-000018 v2：Lean 在 Mathlib 上证明指数 20863/20000 = 1.04315 的序列型 unit-distance 结论，但条件于一个关于固定 8192 次数域 E_W 的显式 Dedekind-zeta 数值不等式 H_W；H_W 本身由 Lean 外的 rigorous certificate 计算验证。Palomar 用 Lean kernel、NanoDa 与 con-ron 重放 proof，并明确把自动 statement review 与人类同行评审区分开。
数学发现
推荐理由：这是五月 AI 反驳 unit-distance 猜想之后一个实质 follow-up：指数继续改善，AI 参与研究设计与证明开发，同时把核心定理压缩到可独立 statement-check 的 Lean surface。Radar 同时保留关键边界：形式证明仍条件于一个外部数值不等式，其 certificate 虽可重放，但并未纳入 Lean 内核证明。
08:00
Palomar / GitHub 精选 AI 评分 92 ☆ P. M. Aronow 与 Patrick Lopatto 将 rough random design 下 constant conditional variance estimation 的主要 minimax 结果完整打包进 Lean：包括 s>1、d>4s 时的 refined minimax bracket、exponent limit、eventual polynomial bounds，以及低 smoothness 与 parametric regimes。仓库披露原始 development 由 Sol 6.1 autoformalize，后续 Codex 负责 Palomar 准备、compiler compatibility 与 automated review。PALOMAR-2026-10-10-000002 于 10 月 10 日注册，Challenge 仅依赖 Mathlib / Lean core；五个 paper-level statements 由 Lean kernel、NanoDa 与 con-ron 接受，并附 automated statement review。作者明确说明这些机器检查不推导出 human mathematical review。
形式化数学
推荐理由：这是 research-level statistics theory 被大模型大规模 autoformalize 后进入独立 registry / multi-kernel verification 的代表案例。贡献不在于 10 月 10 日新发现统计定理，而在于把既有研究结果转换成可独立检查的 Mathlib-only statement surface 与 durable proof artifact。
10月9日 ⌄ 星期五 · 5 条
18:55
aiXiv / GitHub 精选 AI 评分 91 ☆ Oleksiy Babanskyy 给出四元三向日葵自由简单集合族的 computer-assisted 上界：若把空 kernel 也计入 forbidden three-sunflower，则最大规模 M(4,3) 满足 54 ≤ M(4,3) ≤ 68，因此任意至少 69 个四元集合的有限简单族必含三向日葵。作者披露 OpenAI Sol 5.6、Astra 6、Pro 6、Sol 6.1 等 AI 工具参与 proof development、软件准备与 manuscript review；公开 companion 固定输入与 42 个有限检查 suites，complete replay 在普通与 Python -O 模式下均通过。项目明确保留边界：没有排除 68、没有证明 54 最优，也没有解决一般 sunflower conjecture；计算 replay 也不等同于独立专家审查或端到端形式证明。
数学发现
推荐理由：这是明确的新极值组合数学上界，并把 AI-assisted proof development 与精确整数/有理数计算 companion、固定 commit、完整 replay receipts 连接起来。其验证边界也写得清楚：可重放有限计算显著强于纯文本声明，但不能替代对数学归约和外部输入的独立人工核验。
08:00
Thomas Hales / Terence Tao 精选 AI 评分 94 ☆ Thomas Hales 10 月 9 日在 Terence Tao 博客发表长文，系统解释 Lean proof 的 elaboration / kernel trust model，并强调“kernel 接受”不能自动证明形式陈述忠实表达原数学问题：AI 时代还必须审计 definitions、theorem statement、未经授权公理与 informal-to-formal correspondence。文章回顾 2026 年 Lean soundness bugs、AI 辅助发现 kernel / elaborator 问题的案例，讨论 Comparator、独立 kernels 与 Con-Leche 等交叉检查路线；Hales 同时指出，在其判断下截至 2026 年 10 月仍缺少覆盖 Lean abstract type theory 的完整公开 relative-consistency proof，并主张 foundational trust claims 需要比单个 kernel run 更强的公开证据。
工具与生态
推荐理由：随着 AI-generated Lean artifacts 快速扩张，Hales 这篇专家方法论文章直接界定了“形式化已验证”应该被怎样理解：kernel soundness、statement fidelity、axiom discipline 与 cross-checking 是不同层级的证据。它对 AI4Math 的评价与发布规范具有直接制度价值，而不是普通观点评论。
08:00
Nicolas Brosse / Human–AI Mathematics 精选 AI 评分 90 ☆ Nicolas Brosse 于 10 月 9 日公开 Human–AI Mathematics framework 的首个 case study：自 6 月起用多轮 AI agents 搜索 Kannan–Lovász–Simonovits conjecture，并在 10 月初三支外部 human-AI 团队陆续给出 KLS 证明后，于两天内分别把这些证明重建进统一 manuscript / ledger 并做内部 certification。框架把 researcher、reviewer、writer 分离，要求 claim 只有在 fresh-context independent review 或具名人类明确接受后才能从 open 升级为 proved；每次认证绑定 statement / proof fingerprint，修改后自动 stale。项目公开披露早期 agent reviews 曾漏掉 false endpoint、错误蕴含方向和具体反例，fresh-context re-review 才发现并修复；当前 KLS manuscript 的 certification 仍是 agent review，不等同于期刊审稿或人类数学家独立阅读。
工具与生态
推荐理由：它把长期 multi-agent 数学搜索中的 provenance、失败记忆、claim state、review independence 和 human handoff 变成显式协议，并公开了真实失败案例。其价值不在于再次宣称解决 KLS，而在于提出一个可审计、可参与的 agentic mathematics research workflow，同时诚实区分 traceability 与 correctness。
01:12
arXiv / GitHub 精选 AI 评分 97 ☆ Scott Armstrong、Ahmed Bou-Rabee 与 Tuomo Kuusi 研究 log-correlated random potential 中 Brownian particle 的弱无序极限，证明其缩放极限相对 Brownian motion 奇异、可逆测度由 Gaussian multiplicative chaos 给出，并建立 quantitative homogenization、anomalous exit-time scaling 与 large-scale Hölder / Liouville 结果。配套 Lean 4 library 含 5,884 个文件、1,592,483 行，覆盖论文主要定理；公开仓库披露 Claude、OpenAI GPT 以及部分 DeepSeek、Mistral、GLM 模型参与 Lean 编写。项目报告无 `sorry`、无 `native_decide`、无新增公理，并用 Mathlib-only restatements、axiom audit 与 Lean/NanoDa/con-ron Comparator 检查主陈述。
形式化数学
推荐理由：其规模、概率/PDE 技术深度与公开审计链使它成为 AI-assisted formal mathematics 的高信号案例：不仅 kernel-check proof，还提供 paper-to-Lean correspondence、standard-axiom audit、clean build 与多 kernel comparator checks。
00:18
Baiying Liu 在 OpenAI 近期给出的 quasi-Riemann 7/8 zero-free half-plane 证明框架上重新优化参数 b 与 ℓ，将边界从 0.875 改进到 (1507−2√921)/1653 ≈ 0.874957069799。论文明确披露 OpenAI Codex（GPT-6.1 Sol Medium-Ultra）参与 drafting、source checking 与 improved-bound search，Claude Opus 5.5 Medium 参与 auditing；结果同时给出 Lean formalization。改进幅度很小，但它证明原始参数选择并非最优，也展示了 frontier-model result 发布后由人类 + AI 快速复核、局部优化并形式化的后续研究模式。
数学发现
推荐理由：绝对数值增益虽小，但这是对刚公开的重要 AI 数学结果的独立、可检查 follow-up：AI 帮助搜索参数，人类作者负责研究结论，Claude 承担审计，Lean 固定最终数学陈述。其价值更多在于可验证的 follow-up research loop，而非改进幅度本身。
10月8日 ⌄ 星期四 · 2 条
20:50
arXiv / GitHub 精选 AI 评分 95 ☆ Scott Armstrong、Benny Avelin、Tuomo Kuusi 与 Aatu Turpeinen 将 De Giorgi–Nash–Moser 理论推广到可能退化且无界、但满足 coarse ellipticity 条件的对称系数椭圆方程，并证明系数范围、局部界中的粗椭圆比幂次及 weak Harnack 指数范围的 sharpness。配套 CoarseDeGiorgi Lean 4 development 约 10 万行、约 1,000 个 modules；仓库明确披露 Lean 代码由 AI agents 在作者监督下完成：Claude Opus 5.5 负责协调和审计，GPT-6 Luna / Sol / 6.1 Sol 与 Claude Sonnet 5 编写 Lean。项目报告无 `sorry`、无自定义公理，并以 Mathlib-only restatements 和 leanprover/comparator 独立检查主陈述。
形式化数学
推荐理由：这是一项 research-level nonlinear/elliptic analysis 规模的 AI-assisted formalization，而不是孤立 theorem translation。公开 provenance 清楚区分作者的 statement review、agent 编码与 agent audit，并用 axiom audit 和独立 comparator statement checks 补强可验证性。
08:00
Retraction Watch / OpenAI 精选 AI 评分 94 ☆ Retraction Watch 10 月 8 日独立报道 OpenAI 在大规模数学稿件发布后撤回 3 篇预印本：核心问题是一篇关于 split abelian eightfolds 的稿件在 stabilization-trace cancellation 中出现符号错误，该错误同时破坏了另外两篇依赖论文的构造。OpenAI 还修订了 14 篇稿件，涉及 proof repairs、statement corrections、hypotheses / dependencies 澄清与引用修正。OpenAI 发言人称错误由内部 audit 发现，并确认这批稿件中大约 50% 在发布时尚未得到确认；公司表示会持续更新 formalizations、errata，并在无法修复时撤稿。
工具与生态
推荐理由：这不是对 10 月 6 日 `openai/math` 发布的普通二次报道，而是独立核实了结果集合发生实质性状态变化，并新增 OpenAI 对审核流程与“约半数结果发布时未确认”的公开说明。对于 AI-generated research at scale，撤稿、修订与 verification-state disclosure 本身就是高价值治理和证据事件。
10月7日 ⌄ 星期三 · 1 条
08:00
Quanta Magazine 精选 AI 评分 91 ☆ Quanta Magazine 于 10 月 7 日报道，MIT 的 Dor Minzer 与学生 Yumou Fei、Shuo Wang 在 9 月已完成一个与 Unique Games / 2-to-1 games 密切相关的 4-to-1 milestone，但原本仍计划用数月完善写作；当他们得知 OpenAI 可能即将公开 AI 证明的传闻后，为避免被抢先，于三天内仓促整理并发布 95 页手稿。OpenAI 随后在 10 月 6 日的大规模数学结果发布中公开了 AI 生成、Lean-verified 的 2-to-1 conjecture proof。Quanta 的独立采访还记录了研究者对 priority、失败经验价值、长期项目激励和“math by press release”的担忧，使这篇报道成为 AI 能力开始直接改变数学研究发表行为的可核验案例。
工具与生态
推荐理由：这不是对 10 月 6 日 OpenAI 数学发布的普通二次转述，而是由 Quanta 通过具名采访首次补充了一个此前未公开的、可具体追溯的生态后果：仅凭 AI proof 即将发布的预期，就足以改变人类团队的 publication timing 与 manuscript quality trade-off。它直接影响 mathematical priority、研究激励与长期项目风险，是 AI4Math 从能力展示进入科研制度层面的高信号事件。
10月6日 ⌄ 星期二 · 2 条
21:22
Zhou 与 Li 提出 SCOPE（State-Conditioned Operator Planning and Execution）：语言模型不直接生成完整 Lean proof，而只在受限 operator vocabulary 上做 state-conditioned 规划，符号引擎执行数值计算、编译器生成最终证明，从架构上规避多步数值证明中“任一整数出错即整体失败”的误差累积。论文在 218 题 suite 上使用 135M backbone 认证 191 题（87.6%）；7B DeepSeek-Prover-V1.5-RL 认证 18 题且消耗 27.5 倍 tokens、37.5 倍 wall-clock。SCOPE 还在 Lean-Workbook 的 3,536 个可评分 admissible problems 中认证 2,132 个（60.29%），并报告 version-frozen review、independent rechecks 与 reverse verification。
定理证明
推荐理由：它把语言模型限制为高层 proof-policy planner，把精确数值执行和最终 proof rendering 交给确定性组件，从而同时获得小模型效率与 Lean certificate。该贡献是可迁移的 neuro-symbolic theorem-proving architecture，而不是单纯扩大模型或增加 test-time sampling 的 benchmark 提分。
08:00
OpenAI / GitHub / AGMAI 精选 AI 评分 100 ☆ OpenAI 于 10 月 6 日公开 `openai/math`：722 篇数学稿件被组织为 372 个 result families，主要由同一个尚未公开的内部 frontier model 在约 4,000 个开放研究问题上的评测中产生，平均每个结果使用约 3 小时 ChatGPT Pro thinking 等价算力。公开目录涵盖数论、组合、几何、拓扑、分析、概率、数学物理与理论计算机科学等方向，其中列出的主张包括 quasi-Riemann hypothesis、Hilbert 第十问题在有理数域上的否定解、Catalan 常数无理性等；仓库同时发布许多 Lean 形式化、Comparator 配置与 10 份删节 reasoning summaries，但 OpenAI 明确说明并非所有结果都已形式化，未形式化稿件可能存在问题。独立的 AGMAI 同日称这是“对数学具有重要后果”的事件，但强调其咨询不构成结果背书，并把公开视为人类理解与社区评估的开始而非完成。
数学发现
推荐理由：这不是单个 benchmark 分数或单篇 AI-assisted paper，而是一次前所未有规模的 frontier-model research-mathematics release：同一评测管线从约 4,000 个开放问题筛出 372 个结果族，并把论文、版本化引用、部分 Lean 证明和有限 reasoning provenance 同时公开。其潜在数学影响极高，但证据状态高度不均一，因此 Radar 将它记录为“大规模公开研究主张与形式资产”的里程碑，而不把 722 篇稿件等同于 722 个已经独立确认的数学突破。
10月5日 ⌄ 星期一 · 2 条
10:25
Jiang、Vempaty 与 Jagmohan 提出 SO-RSI，把 agent workflow 的 recursive self-improvement 从“看到失败就局部改参数”的一阶修补，升级为先识别 recurrence、opposing edits 与 expectation mismatch 三类结构异常，再通过 lightweight diagnostic probes 和跨轮次 persistent inquiry memory 积累因果证据后修改工作流。论文在匹配的 24 小时搜索预算下报告：相较 Naive RSI，Lean 4 proof generation 的最终 held-out pass rate 提高 21.8 个百分点，Verus verifiable-code generation 提高 25.8 个百分点；消融实验也显示 executable probes 与 persistent investigation memory 都是主要增益来源。
定理证明
推荐理由：它不是一次普通 Lean benchmark 刷分，而是把“如何改进 prover agent 自己的工作流”变成可诊断、可积累证据的二阶优化问题，并用 Lean 4 与 Verus 两种可验证环境验证机制增益。对长期运行的 theorem-proving / formal-verification agents，这比单次 prompt、搜索或模型升级更接近可迁移的 agent-learning 方法。
00:48
Jana 等提出 AIProver：联合后训练 119B 开放权重模型并用 HarnessEvolve 进化可调用 Lean 工具的 agent harness，把 type correctness、proof completeness 与 semantic correctness 都纳入 verifier certificate。工作同时发布 LoCoBench，含 5.89 万个来自 Mathlib、CSLib、Mizar 与 bounded arithmetic 的实例，其中 771 个验证样本没有公开 Lean 形式化；论文报告在 Leanstral-1.5 基座上 semantic-correct pass@4 从 15.7% 提升到 36.7%，并把同一能力封装成 Claude Code / Codex skill，在对应评测中分别将 semantic correctness 从 41.9% 提升到 79.8%、从 34.1% 提升到 62.4。
形式化数学
推荐理由：它把 research-level autoformalization 的关键可信性缺口——“Lean 能编译”不等于“忠实表达原数学命题”——直接写入训练与验证目标，并把开放权重模型、agent harness evolution、语义正确性证书和新 benchmark 连成一个可复用研究栈；价值不只是单一 theorem-proving 分数提升。
10月4日 ⌄ 星期日 · 2 条
23:45
Hasan、Jain 与 Samin 提出 Discovery–Execution（DE）框架，用短预算解题尝试估计 strategy discovery，再用给定 oracle sketch 的条件运行估计 strategy execution，从而预测增加 test-time compute 后的数学成功率。论文在 4 个模型、35 道新鲜 Olympiad 题和非几何 IMO-ProofBench Advanced 上测试：GPT 系列呈现接近饱和 execution 的几何 scaling，而对 Claude Opus 4.8 显式测量 execution 可显著改善外推；基于 DE 的 continue / restart 决策在实验中也取得低于最佳模型特定事后策略的平均 regret。
评测与数据
推荐理由：这不是普通 benchmark 排名更新，而是把“多给推理时间为什么会有效”拆成可测量的 discovery 与 execution 两个瓶颈，并进一步用于预测 scaling 与分配推理预算；它为数学 reasoning 的 test-time compute 评价提供了可迁移的方法学。
09:04
James Chang · GitHub / Palomar 精选 AI 评分 95 ☆ James Chang 公开一份由 OpenAI Dots 数学研究 campaign 产生的 covering-design 结果：证明 C(24,14,4) ≥ 20，并由 Schönheim bound 推出 C(25,15,5) ≥ 34，分别改进此前 19 与 32 的公开下界。项目说明 10 月 1–3 日由 1 个 coordinating dot 与 6 个 Astra research subagents 开展数学探索和 Lean 形式化，Chang 负责选题、研究指导与路线判断；公开仓库随后提供 Challenge / Solution、约 8,800 行 Lean、fresh rebuild 与 Comparator 检查，Palomar 于 10 月 4 日登记固定提交并重放 Lean 及独立 kernel 检查。维护者同时明确说明尚无数学家完成独立人工审查，而且两个 covering number 的精确值仍未确定。
数学发现
推荐理由：它同时满足“新的数学下界 + 明确的人机 provenance + 可公开检查的 Lean artifact + 独立 registry 重放”四个高信号条件，是 agentic mathematical research 从探索到可审计形式证据的代表案例；但当前证据层级仍应停在 machine-checked artifact，不能替代尚未发生的独立数学家审查。
10月3日 ⌄ 星期六 · 1 条
23:59
aiXiv / public repositories 精选 AI 评分 90 ☆ Oleksiy Babanskyy 于 10 月 3 日公开两篇数论论文，分别证明 Zhi-Hong Sun 2021/2022 列出的 supercongruence Conjectures 3.5 与 3.6，涉及 Apéry-like binomial sums 模 p² 的精确同余。作者披露 OpenAI Codex 与 GPT-6.1 Sol 在其指导下参与数学探索、proof criticism、source comparison、exact computation、consolidation 与写作；两篇均提供公开源码、精确算术 companion 和复核过程。其中 3.5 companion 对 301 个素数到 1999 的数据、endpoint checks、invariant / modular polynomials 等做 fresh replay；3.6 companion 同样执行大规模 exact checks。作者明确说明这些检查不等同于独立专家审查、端到端形式证明或优先权认证。
数学发现
推荐理由：这组工作展示了 AI-assisted mathematical research 在一个具体数论问题族中从 conjecture targeting、proof exploration 到 exact computational audit 的完整公开链条。两篇论文解决的是明确的既有猜想，并提供可复查的 companion artifacts；但由于没有独立 specialist review、formal-kernel proof 或完整 priority certification，Radar 只把它记录为作者负责、AI 深度参与且带精确计算复核的研究结果，而不升级为已独立确认的最终结论。
10月2日 ⌄ 星期五 · 1 条
08:00
Meta AI Research 精选 AI 评分 97 ☆ Meta AI Research 于 10 月 2 日发布一组由数学家与 Muse Spark 1.1 / 1.2 Thinking Mode 协作完成的 6 篇数学研究论文，覆盖概率、微分方程、群论、优化、算术物理和非结合代数，其中 5 篇给出此前开放研究问题的答案。研究者通过普通 meta.ai 聊天界面工作，没有定制 research scaffold；每个项目由数学家选择问题、引导研究并完善论证，随后由第二组数学家复核。论文还区分主要由研究者起草与主要由 AI 起草的段落，并明确承认部分问题存在同期独立工作。
数学发现
推荐理由：这是 AI 从 Olympiad-style benchmark 走向真实开放研究数学的高信号人机协作案例，而且 provenance 相对透明：普通聊天界面、无定制 scaffold、数学家主导问题与论证、第二组数学家复核、AI/人类文本贡献标记、并承认同期独立结果。Radar 将其记录为 human-AI collaborative research milestone，而不是 autonomous solve。
10月1日 ⌄ 星期四 · 2 条
22:42
Zhou、Yang 与 Zhang 提出 mutation-enhanced skill self-evolution framework，同时演化 Lean prover 的高层 solving policy 与 reference knowledge。普通 skill evolution 往往依赖成功/失败轨迹对比；SkillEvoLean 在所有 sampled trajectories 都失败时，会采样数学概念生成新的 skill candidates，并用 Lean verifier feedback 选择 mutation。论文在相同 backbone、trajectory budget 与 test-time compute 下，使用 GPT-5.5 报告 MiniF2F 100.0%、PutnamBench 90.6%、IMO 2025 4/6、USAMO 2026 4/6；concept-guided mutation 相比 random-text mutation 在 MiniF2F 和 PutnamBench 分别提高 6.9 与 8.2 个百分点。
定理证明
推荐理由：它把 agent skill evolution 明确引入 formal theorem proving，并解决了一个实际瓶颈：当一次搜索完全没有成功 proof trajectory 时，系统仍能利用数学概念与 verifier feedback 产生新的求解策略，而不必更新模型参数。
09:00
Lwin 提出 FORALL-LEAN-AGENT，一个面向 Lean coding agents 的 frontend-agnostic 审计框架。它将隔离工作区、Lean 工具、fresh review、statement comparison、axiom audit 与可用时的 independent proof checking 绑定到同一个 candidate artifact，使 acceptance decision 可追溯，而不把“成功编译”直接等同于“证明了预期命题”。论文在 VeriSoftBench、PutnamBench 和 Lean Eval software-verification track 上评测；在 100-task VeriSoftBench subset 中，GPT-5.6 Sol 的 benchmark-rule success 从 93 提升到 100，同时报告成本从 69 美元降到 62 美元；PutnamBench 672 题全部通过框架 acceptance，平均每题 4.72 美元。
形式化数学
推荐理由：它直接处理 AI formalization / proving 中最关键的可信性缺口之一：typecheck 只说明某个 formal artifact 被 Lean 接受，不能自动证明 statement fidelity、assumption hygiene 或独立复核已经成立。该工作把这些检查变成可执行、可追溯的 agent acceptance protocol。
9月30日 ⌄ 星期三 · 3 条
22:00
DIMACS / Rutgers 精选 AI 评分 84 ☆ Peter Zenz 在 Rutgers AI and Mathematics Seminar 介绍 BruKnot，一个面向困难 unknot diagram 的 neuro-symbolic 系统。它把 Reidemeister moves 的符号搜索与微调语言模型结合：常规简化停滞时，模型提出短的 crossing-increasing 与 rearrangement 序列，作为继续搜索所需的辅助构造。报告同时讨论训练数据管线、learned guidance 与 symbolic search 的交互、当前困难及向其他数学领域推广的可能性。
数学发现
推荐理由：该工作针对数学推理中的关键瓶颈——发现有用辅助构造——给出明确的 neuro-symbolic architecture，而不是把 LLM 仅作为答案生成器；目前证据是正式研究 seminar 摘要，因此收录其系统设计信号，不声称已有论文级实验结论。
08:00
UW Math AI Lab 精选 AI 评分 82 ☆ University of Washington Math AI Lab 的 Fall 2026 项目周期于 9 月 30 日开始，共列出 15 个项目，覆盖 AI-assisted proof discovery、Lean evaluation、Math2Vec、autoformalization、agentic math education 等方向。该实验室同时维护开放问题地图、TheoremSearch 与长期项目档案，形成研究、工具和人才培养结合的 AI4Math 社区基础设施。
工具与生态
推荐理由：单个学生项目未必都是重大事件，但 15 个并行 AI4Math 项目与持续开放工具共同构成值得追踪的研究生态信号，适合作为 Radar 的生态类条目而非突破性结果。
08:00
Scientific American 精选 AI 评分 96 ☆ Scientific American 9 月 30 日报道，Anthropic 的 AI 系统给出了长期悬而未决的 Bernoulli bond percolation 临界连续性证明：对整数格 ℤ^d 的中间维度情形，临界点处不存在无限开簇，从而补齐此前只在二维和高维已知的连续性图景。报道援引领域研究者评价，并指向 Anthropic 公开的 Lean 形式化；公开材料同时强调该工作尚未经过独立同行评审，机械检查不能替代对 formal statement 是否忠实表达原问题的人工核验。
数学发现
推荐理由：这是对一个重要概率论长期猜想的高质量独立新闻报道，新增了领域专家反应并链接到公开 Lean 证据；Radar 将其作为 9 月 30 日的独立报道收录，而不把媒体措辞升级成已完成传统同行评审的最终认证。
9月29日 ⌄ 星期二 · 2 条
08:00
Advisory Group on Mathematics and Artificial Intelligence（AGMAI）在 9 月 29 日发布面向 AI labs 的数学成果发布建议。文件基于 600 余份数学界反馈，区分“有人类数学家完全理解并负责”的论文与“尚无人真正理解”的 AI 输出；后者应及时公开、补足文献归因与传统论文式表述，并披露模型、prompts、耗时、估算计算成本、失败尝试背景与 formalization status。AGMAI 还建议尽可能提供 comparator / formalization metadata，并由 AI labs 资助社区主导的人类理解工作。
工具与生态
推荐理由：这不是单一模型或证明结果，而是 AI4Math 社区开始建立可操作的学术发布与验证规范；其要求与本 Radar 已采用的 evidence discipline、形式化边界和过程可审计性直接相关。
08:00
arXiv / GenLimitLib 精选 AI 评分 88 ☆ GenLimitLib 在 9 月 29 日提交预印本，围绕由 Kleinberg 与 Mullainathan 引出的 language generation in the limit 理论构建 source-aligned Lean 4 library。作者报告 formal developments 覆盖 30 篇论文，并抽取共享定义、可复用证明组件和跨论文关系，同时通过数学案例与 LLM 实验讨论其对 paper understanding、conjecture generation、theorem proving 与 paper-to-Lean 的支持。
形式化数学
推荐理由：它把一条快速扩张的 LLM 理论文献线整理成可机器检查、可复用、跨论文对齐的形式资产，并明确服务于 AI-assisted mathematical research；价值在基础设施和研究地图，而非单篇定理刷分。
9月28日 ⌄ 星期一 · 4 条
15:17
MathAgent 构建 MathKG，将 Mathlib 定理和定义连接成带类型的语义知识图谱，并在五个模型、四种 augmentation 模式上做 controlled ablation。论文报告 Lean specialization 的收益远大于任何单一 augmentation，同时知识图谱帮助小模型却可能伤害大模型；但不同 context 模式在题目层面具有明显互补性，oracle 选择可进一步提升困难 benchmark 的 solve rate。
定理证明
推荐理由：它没有停留在“加检索是否涨分”的单点比较，而是用能力分层和四路 ablation 展示 augmentation 的条件性与互补性，对设计自适应 theorem-proving agents 和检索策略有直接方法学价值。
08:00
FrenzyMath 宣布完成 Poincaré 猜想的 Lean 4 形式化，并称这是其所知首个同时通过完整 Lean build 与 Comparator 验证的版本。当前公开仓库 README 已将项目标记为 complete，记录 Comparator 在指定 commit 上接受公开目标，并由 Nanoda 与 Lean 默认 kernel 检查；团队称数学家与 AI agents 在约半个月内协作完成大部分工作。
形式化数学
推荐理由：这是经典重大定理的大规模 AI-assisted formalization 里程碑，而且当前公开仓库已从早期 incomplete 状态更新到 complete，并给出可检查的 build / Comparator / kernel evidence；Radar 仍把它理解为既有数学证明的形式化，而非新的 Poincaré 猜想证明。
08:00
Vals AI 报告让 10 个 Claude Sonnet 5.5 agents 并行研究 Thomson problem 在 N=7 时的最优构型，约 15 小时后生成 17,895 行 Lean 证明，证明正五角双锥是七个单位电荷在球面上的最低能量构型。官方博客称该证明被 Lean 接受，并由第二个 kernel 实现复核；它把多 agent 数学搜索、长形式证明生成与 kernel verification 串成一次公开实验。
形式化数学
推荐理由：这是 9 月 28 日最清晰的 AI4Math 新事件之一：不是单纯 benchmark，而是多个 frontier agents 在小时级时间尺度内产出一个长篇、kernel-checkable 的数学证明。Radar 记录其公开验证状态，但不把 Vals 的内部实验过程等同于独立外部复现。
01:13
该工作构建 agent-guided proof mutation framework：用 Codex/GPT-5.6 Sol 与 Claude Code/Claude Opus 5 生成会破坏局部论证的逻辑错误，再测试 agentic judges 是否能发现，并把成功绕过 judge 的错误蒸馏成可迁移 mutation strategies。论文报告这些策略在未见 proof 上仍显著提高绕过率，而且 judge 从 Olympiad/研究生教材到研究级数学手稿呈现明显可靠性下降。
评测与数据
推荐理由：AI4Math 的瓶颈已经从‘会不会生成证明’延伸到‘能不能可靠审查证明’。这篇工作用受控错误注入和 held-out transfer 明确测量 frontier judge 的失效模式，对未来 AI 数学结果的人类监督、自动验证和发布规范都有直接影响。
9月27日 ⌄ 星期日 · 3 条
21:29
Palomar Registry 精选 AI 评分 94 ☆ Palomar 于 9 月 27 日登记一个四色定理 Lean 4 / Mathlib 形式化：项目将 Georges Gonthier 的 Coq 证明迁移到 Lean，并明确归因 Claude Opus 5.5 在 Robert D. Barish 指导下作为 AI agent 参与。登记说明该版本以 Mathlib 实数陈述主定理，重写可约配置检查为由 Lean kernel 检查的 bit-parallel certificate engine，并把 Coq tactic case analysis 改为一次证明正确的 checker 所检查的 case trees。
形式化数学
推荐理由：它不是新证明四色定理，而是一次大型经典 proof artifact 的 AI-assisted cross-prover migration，并显式强化了 kernel-checkable computation 与 statement/proof provenance；这对自动形式化和大型 formal corpus 迁移具有直接工程价值。
08:19
Kristian Muri Knausgård 报告将 Riemann ζ 函数不同非平凡零点的下渐近比例下界从约 0.83625 提升到 0.8369928814。新证明使用带自由截断参数的矩阵不等式强化能量下界，关键矩阵不等式、threshold lemma、block dichotomy、counting assembly 和精确算术均在 Lean 4 中形式化。论文明确称这项工作‘主要是一次 AI-assisted mathematical research 实验’，同时保留一个来自近期工作的 computer-assisted local inequality 输入，该输入尚未经过正式同行评审。
数学发现
推荐理由：这是 AI 辅助研究进入前沿解析数论、同时把关键证明块落到 Lean 的代表性结果；但常数仍依赖一个未正式 referee 的 computer-assisted local inequality，因此 Radar 不把形式化覆盖范围扩大到所有外部输入。
03:59
该工作把 LeanDojo 一步转移作为自监督信号，用 JEPA-style 模型预测 successor state 的 latent representation，并只在 kernel-validated、nonterminal successors 上做排序。JEPA 在 same-theorem Top-1 排名诊断中明显优于 InfoNCE，但三次种子平均只解出 282.3/987 个定理，低于原 proposer ordering 的 308，而且需要更多 tactic checks。
定理证明
推荐理由：这是一个有价值的负结果：局部 successor ranking 更准确，并不等于长程 proof search 更好。它把 representation quality 与 proposal/search dynamics 分开评估，对 theorem-proving agent 的 value function 设计非常直接。
9月26日 ⌄ 星期六 · 4 条
15:36
VeryMath · GitHub 精选 AI 评分 84 ☆ VeryMath 在 9 月 26 日合并 Co-Mathematician 0.3.0，加入本地 Web workbench、项目与文件夹浏览、多模型服务配置、流式对话、PDF 原页阅读、公式预览、研究笔记和 VeryMath Skills。项目把长期数学研究状态保存在本地文件/仓库中，而真正的计算、证明和独立 review 仍由外部 coding agents 驱动。
工具与生态
推荐理由：这是面向 AI-assisted mathematical research 的完整 workspace 形态，而不是一次性 prompt demo：它把材料、研究目标、会话与可持续项目状态组织在一起，同时明确把执行和验证留给外部 agents，代表一种值得跟踪的 AI4Math research-environment 设计。
12:51
OracleLadder 通过逐级提供 roadmap、milestone answers 与单步 oracle help，定位 LLM 数学推理失败发生在哪一层。论文在 354 个 NuminaMath 问题和 6 个模型上发现，最大的失败类型是 composition gap：模型可以分别完成中间步骤，却仍不能把这些步骤组合成完整解答；该现象在剔除潜在评分错误后仍覆盖约 24%–37% 的问题，并在 MATH500、AIME 2024/25 上复现。
评测与数据
推荐理由：这项工作把‘数学 reasoning accuracy’拆成可诊断的结构性 failure modes，并显示单步能力与全局解题能力存在明显 composition gap；对 agent decomposition、roadmap prompting 和 RLVR 评估都具有直接意义。
12:42
CompassPlay 重新设计 self-play 中 proposer 的奖励：不只奖励“题目有多难”，而是根据候选任务与目标 reference tasks 的 solver gradient alignment 衡量其训练价值。论文在 Lean 4 theorem proving 中报告，达到 difficulty baseline 150 次迭代的累计覆盖时，CompassPlay 可节省约 40% GPU-hours。
定理证明
推荐理由：它把 theorem-proving self-play 的 proposer 从“生成难题”升级为“生成真正推动 solver 学习的题”，并给出算力效率证据，具有明确的 agent-training 工程价值。
02:44
Choir 将大型形式化项目拆成可独立领取的任务，贡献者可用各自的 LLM subscription 和本地 agent 完成子任务，并通过 GitHub 仓库协调。每项贡献在合并前经过 deterministic gate；协议支持 Lean 4、Isabelle 与 Rocq。作者还给出一个 Choir 驱动的教材形式化示例：Yufei Zhao《Probabilistic Methods in Combinatorics》讲义中的 285 个 Lean 4 定理。
形式化数学
推荐理由：它把 autoformalization 从单团队、单算力池的集中式执行，扩展为可公开协作、可验证合并的分布式 agent protocol；这直接触及大规模形式化的成本、并行化和社区参与问题。
9月25日 ⌄ 星期五 · 1 条
08:00
CICM 2026 的 AI4Math Workshop 于 9 月 25 日举行，议程覆盖机器学习调优的自动定理证明、flexiformal LLM-assisted mathematics、Wolfram 纯数学语义表示、PIDE MCP 连接 AI agents 与 Isabelle、10 个可扩展组合数学挑战的 Lean benchmark，以及 AutoGraphForge 的猜想生成—反例搜索—Lean proving 闭环。该 workshop 明确定位于连接 formalization、ATP、数学知识管理与 machine learning for mathematical reasoning 社区。
工具与生态
推荐理由：它不是单篇论文，而是一次高度聚焦 AI4Math 的社区事件：议程直接汇聚 agent 接入证明助手、形式化 benchmark、自动发现和 ATP+ML，多条当前技术主线在同一天形成公开交叉。
9月24日 ⌄ 星期四 · 4 条
17:30
ProofGap 从 B. P. Demidovich《数学分析习题集》3,015 道题的自然语言解答中抽取并对齐局部证明缺口，形成 26,116 个 formal proof gaps。每个任务直接给出局部 Lean context 与 target，把“这一步会不会证明”从整条 proof composition 中拆出来，从而能更精确定位模型的 step-level formal reasoning failure；作者同时指出，这类局部 obligations 未来也可用于 proof-verification pipeline，但仍需要可靠的语义翻译与顺序组合。
评测与数据
推荐理由：当前 formal-math benchmark 大多只报告 theorem-level success，ProofGap 把失败定位到局部 obligation，能区分“单步不会做”和“组合失败”；这与前几天 OracleLadder 的自然语言 composition-gap 结论形成很好的 formal counterpart。
08:00
Marcus J. Min / ProofNet-Verified 精选 AI 评分 95 ☆ 作者 9 月 24 日确认 Ground False 被 NeurIPS 2026 E&D Track 接收。其公开 ProofNet-Verified 审计显示：在 367 个 ProofNet 问题中，原 ProofNet 有 204 个问题存在错误或歧义，ProofNet# 仍有 97 个；其中大量问题来自 informal-to-formal 语义不忠实、缺失前提以及对 Lean/Mathlib 的误解。项目不仅标记错误，还通过证明错误形式化的否定、给出 trivializing proofs 或详细语义分析来确认问题，并发布修正后的 Lean 4 statements 与 proofs。
评测与数据
推荐理由：它直接动摇了 formal-math benchmark 的默认前提：kernel-checkable 并不保证 benchmark statement 忠实于原题。对于评估 theorem provers 和 autoformalizers，这类 ground-truth audit 与模型 accuracy 本身同等重要。
01:40
该工作构造多步函数组合任务：同一组数学规则以不同顺序呈现，但正确答案保持不变。作者在 16 个 1B–8B 语言模型上同时测量准确率与 permutation signal-to-noise ratio（SNR），发现模型越能正确处理规则重排，其内部表示反而越能区分不同顺序；layer-averaged permutation SNR 与准确率在所有设置中均呈正秩相关，最高 Spearman 相关达到 0.86。
评测与数据
推荐理由：它提醒 AI4Math 评测不要把 answer invariance 与 representation invariance 混为一谈：模型可能对等价数学表述给出同样正确答案，同时内部计算路径仍强烈依赖输入顺序。该结果为数学 reasoning robustness 提供了超越最终准确率的表征层诊断视角。
00:06
该工作把定理“有趣性”定义为 proof length / statement length，并显示这一内在指标与定理的下游效用存在较强相关。作者进一步把“给定 premises 后的证明难度”作为基础 primitive，训练一个 27B 模型预测 proof difficulty，并用该信号筛选候选定理。优化这一指标后，生成结果与 Mathlib 的 substantial/full overlap 从 91.9% 降到 30.6%，并演示了候选生成、interestingness selection 与自扩展 formal library 的循环。
数学发现
推荐理由：它把 AI4Math 的目标从“解人类给出的题”推进到“自己决定哪些 formal statements 值得继续证明”，并给出可量化的 theorem-interestingness signal 与 self-expanding library loop，是从 solver 向 research agent 过渡的重要方法学信号。
9月22日 ⌄ 星期二 · 4 条
08:00
该工作指出，LLM theorem prover 通常在 tree search 中部署，但训练仍使用逐 token cross-entropy，目标与有限预算下的搜索成功并不一致。作者将 Compute-Aligned Training 扩展到 policy-guided search，推导出基于 trace 的 search-aware losses，并提出无需指定具体搜索策略的 uniform-allocation loss。Lean 4 / LeanDojo 实验显示，两类目标在 458 个 held-out theorem、6 种 search strategy 上均优于普通 cross-entropy；而且相对收益在更紧的 expansion budget 下更明显。
定理证明
推荐理由：它把 theorem prover 的训练目标从“模仿 demo tactic”推进到“直接优化搜索时真正关心的有限预算 proof success”，并且验证了 search-aware objective 与 test-time compute 的耦合，对 production theorem-proving agent 训练非常直接。
08:00
作者提出 generation-replay protocol：模型先生成数学解答，再重放 prompt+generation 轨迹并提取 reasoning-token activation-importance signatures。对 8 个模型和 5 类数学 reasoning 来源的 40 个 model-source 组合做无监督聚类后，frontier-LLM judges 在 77%–82% 的真实 cluster 中识别出 approach-level coherence，而 matched within-source controls 只有 6%–11%。进一步的 approach-controlled prompting 也能在 8 个模型条件中的 7 个改变 cluster assignment。
评测与数据
推荐理由：它直接挑战按 algebra/geometry/number theory 等 topic 组织数学 benchmark 和训练数据的惯例：即使 topic-balanced，reasoning approach 仍可能严重失衡。对 AI4Math benchmark design、curriculum 和 mechanistic evaluation 都有明确影响。
05:48
PermuFormer 是面向代数组合学 permutation tasks 的专用 autoregressive transformer。作者构建 2.8 billion-token 的 multi-task、multi-encoding corpus 进行预训练，并报告它在预训练未见的基础任务和更复杂的 research-level downstream tasks 上，常常优于从头训练的同架构模型、MLP baselines 和相近规模的通用语言模型。论文同时分析了模型内部表征，显示部分任务可直接从 prompt representation 线性解码，而另一些需要经过多轮生成后答案信息才显现。
数学发现
推荐理由：它代表一条不同于通用 frontier LLM 的 AI4Math 路线：直接在数学对象和多种 permutation encodings 上学习领域表征，并把 specialized pretraining 用到 research-level algebraic-combinatorics tasks。
01:57
arXiv / Lean Pool 精选 AI 评分 89 ☆ Lean Pool 是一个用于保存已完成 Lean 4 形式化项目的开放仓库，论文将其定位为由 AI agents 增长、维护和优化的形式化数学 archive。项目处在 Mathlib 的统一库模式与单纯 registry 之间，持续维护独立 formalization projects，并提供搜索、文档与兼容性维护等能力。
工具与生态
推荐理由：它把 agent 能力从一次性生成证明扩展到长期维护 formalized mathematics corpus，触及 AI4Math 最重要的基础设施问题之一：如何让机器生成资产持续可构建、可搜索、可演化。
9月21日 ⌄ 星期一 · 2 条
21:19
The Endless Exam 提出 14 个参数化 mathematical-construction families，并为每个提交对象提供自动 validity check 和相对 published frontier / baseline 的连续质量评分，且评分不在 1 处封顶。作者在 8 个模型、69 个实例上测试，发现现有系统都未超过已发表 frontier，但连续 size–quality curves 能比 pass/fail 更细致地区分进展。项目公开 generators、verifiers、references、model responses 与分析。
评测与数据
推荐理由：它把 AI4Math benchmark 从固定答案题推进到可随参数规模持续扩展、带 compact certificates 的数学构造任务，并允许未来模型在 published human frontier 之上继续获得可比较分数。
08:00
AGMAI / OpenAI 精选 AI 评分 91 ☆ 9 月 21 日，Advisory Group on Mathematics and Artificial Intelligence（AGMAI）宣布成立并由 Institute for Advanced Study 托管。该组由数学家独立运行，不接受 AI 公司付费，并承诺公开其建议；其成立契机是 OpenAI 曾联系部分成员希望建立外部 advisory board，双方随后同意改为一个独立组织。当前首要任务是就 OpenAI 所称内部模型产生的大量重要数学结果的协调发布提供建议。
工具与生态
推荐理由：这是 AI4Math 从单次能力展示走向独立研究治理与公开问责的重要制度化事件；同时必须准确保留其独立性，不能把 AGMAI 描述成 OpenAI 内部委员会。
9月20日 ⌄ 星期日 · 3 条
08:00
FrenzyMath 报告完成 Renrui Qi 关于 Laver function 的大型 Lean 形式化：在 I3 公理下，其增长超过相关 fast-growing hierarchy 阈值，从而总性不能在 PA 中证明。项目使用基于 Opus 4.8 的专用 agents 与持续人工引导，公开仓库约 36k 行；文章称目标结果及依赖 sorry-free、通过 comparator，并且形式化过程发现并反馈了原稿中的若干可修正问题。
形式化数学
推荐理由：该案例不仅把长证明机器化，还显示 AI-assisted formalization 能发现定义与论证细节问题并反馈到人类论文，是“verification 改善数学成果”的高价值样本。
08:00
Vals AI 9 月 20 日发布 C-HD：10 个 Claude Opus 5.5 agents 在约 15 小时、733 条共享消息后提出一个针对有向、非负实权单源最短路的确定性算法，并生成 Lean 4 正确性与运行时间证明。冻结 proof package 记录了 2,548-job full build、fresh-copy rebuild，以及两次分别检查 18,994 个 project constants 的 kernel replay；形式化改进适用于特定稀疏密度区间，例如沿 m≈n·log^(3/4)n 时给出 O(n·log^(11/12)n) 上界。
数学发现
推荐理由：这是少见的“多 agent 提出新理论算法 + 形式化复杂度证明 + 可审计 proof package”公开案例。Radar 保留其边界：改进是特定密度下的渐近上界，常数巨大，不代表实际运行更快；外部理论计算机科学同行评审当时也尚未完成。
03:42
Open Problems in Numerical Linear Algebra 精选 AI 评分 92 ☆ Open Problems in Numerical Linear Algebra 在 9 月 19 日发布 MI-27 的完整 Lean 4 verification。该形式化覆盖原始 coefficient-one 上界的全维度正定矩阵陈述，不加入额外交换性或谱条件。公开记录称 George Stepaniants 在 substantial OpenAI Codex assistance 下完成形式化；源码通过 source-matched Linux build、Comparator statement matching、Lean default-kernel replay，并对 20 个 frozen contracts 保留 rejection controls。全部导出仅依赖 Lean 标准的 propext、Classical.choice 与 Quot.sound。
形式化数学
推荐理由：底层解析证明在 9 月 12 日已完成，但 9 月 19 日新增的是完整、可审计的 formal verification milestone：它把一个开放矩阵不等式的最终陈述、证明依赖与 rejection controls 固定到机器可检查 artifact 中，并明确披露 AI 在形式化中的实质参与。
9月19日 ⌄ 星期六 · 1 条
09:27
该工作提出 Self-Organizing Agent Teams（SAT）：固定成员的 agent team 不预设专家角色或分工，而是从历史协作中学习可复用的组织策略，包括角色形成、对话阶段、参与模式和信息流。作者仅用 15 道 AIME 2024 数学题和 25 道研究生级知识题学习策略，再原样迁移到未见 benchmark。跨 5 个数学与物理 benchmark，团队平均准确率为 66.7%，高于最强单体 48.8%、compute-matched 单体 58.7% 和 perfect router 59.0%；在 AIME 2026 上高出 perfect router 13.4 个百分点。
评测与数据
推荐理由：这项工作不是简单 majority vote，而是让协作结构本身成为可学习、可迁移的 agent capability，并证明团队有时能组合出任何成员独立尝试都没有得到的数学解答；对 AI4Math multi-agent reasoning 和 verifier-aware collaboration 很有方法学价值。
9月18日 ⌄ 星期五 · 3 条
08:00
SAIR / Terence Tao 精选 AI 评分 93 ☆ Terence Tao 9 月 18 日宣布，Foundation for Science and AI Research（SAIR）将加速推进 Open Math Model initiative：与学术界和产业伙伴合作建设面向科学、尤其数学研究的 open-weight models，以及同时服务开源和闭源 LLM 的 open-source scientific tooling。该计划强调社区参与研究优先级、模型开发与评测，并寻求资金、算力、专业知识和 community-building 伙伴。
工具与生态
推荐理由：这是对当前封闭 frontier math systems 的直接制度与基础设施回应：目标不是一次性 benchmark，而是把可检查、可运行、可教学、可改进的开放数学模型与工具交给数学共同体共同建设。
08:00
Transformer Lab / Maplesoft 精选 AI 评分 85 ☆ Transformer Lab 与 Maplesoft 在 9 月 18 日宣布 Primus for Math，一个面向数学与工程问题的 autonomous research system。官方介绍称系统可从高层问题出发，自主阅读领域文献、推导模型、运行 simulation，并向用户展示过程与结果；产品当天已面向 Primus account 开放。其定位是把此前主要存在于 frontier labs 内部的长程数学研究 agent workflow 产品化。
工具与生态
推荐理由：它代表 AI4Math 从论文和内部实验向可供研究者直接使用的 autonomous research product 迁移。Radar 只记录产品能力声明与发布事实，不把厂商对“frontier discovery”的宣传视为独立验证过的科研结论。
01:54
Bérczi、Dughmi、Livanos、Soto 与 Verdugo 证明线性拟阵上的 matroid secretary problem 具有 1/e 保证，从而解决该类拟阵中的 strong secretary conjecture；结果在线性拟阵预先已知或有限域线性表示在线给出的情形都成立。论文的 concurrent-discovery disclosure 明确写道，主证明于 9 月 15 日在与 ChatGPT-6 Astra 的对话中获得；作者在 9 月 17 日投稿前又发现 9 月 16 日已有独立团队发布几乎相同方法的同一结果。
数学发现
推荐理由：这是 AI 直接参与组合优化/拟阵理论证明发现的高价值案例，同时公开记录了并发独立发现，因而特别适合观察 AI 时代的 provenance、priority 与 attribution 问题。Radar 不把 Astra 归因升级为可独立审计的自治性结论。
9月17日 ⌄ 星期四 · 5 条
23:28
arXiv / Axiom Math 精选 AI 评分 94 ☆ Huang、Lau 与 Ono 证明 Huang–Jiang–Oblomkov conjecture 对所有互素 1<a<b 的 torus-knot singularity X^a=Y^b 成立。主结果是一个更强的 finite identity，把 rank-N HJO sum 与有界 balanced cylindric partitions 的生成函数联系起来，取 N→∞ 得到原猜想。论文同时说明，AxiomProver 已在 Lean 中形式化该 finite identity 与 HJO conjecture，但形式化明确以两个已有文献结果作为条件输入。
数学发现
推荐理由：这条把新的研究数学结果与 AI-generated formal certificate 连接在一起，并且论文清楚披露形式化的条件依赖。Radar 因此将数学证明本身与 AxiomProver 的形式化覆盖范围分开描述，不把条件化 Lean certificate 说成从第一原理完全闭合。
15:26
FormalFlow 通过共享 blueprint 和嵌套 planning、proving、review loops 协调 AI proving agents，在 human supervision 下完成 MIP* = RE 核心量子 soundness 定理的 Lean 4 machine-checked proof。作者报告项目历时 63 天，最终库包含 126,367 行 Lean 代码，并称这些代码全部由 agents 生成。
形式化数学
推荐理由：它直接展示 long-horizon agent orchestration 如何处理大型形式化中的 statement drift、proof composition 与 review，是 Agent + formal mathematics 的代表性工程成果。
13:42
Xinglong Wu 对 Talagrand 的 operator cotype 问题给出否定答案，并且已经在 q=2 时构造出反例：Rademacher cotype 不能由 Gaussian cotype 与 (q,1)-summing norm 的最大值作统一控制。论文摘要最后一句明确写道，反例由 ChatGPT（GPT-5.6）发现。
数学发现
推荐理由：这是非常清晰的 AI-attributed counterexample discovery：关键对象本身被作者直接归因给模型，而不是仅用 AI 润色或形式化。不过公开 provenance 目前主要就是作者摘要中的一句归因，缺少 transcript 或独立 artifact，因此 Radar 只记录作者声明。
00:40
Captain Sude · GitHub 精选 AI 评分 94 ☆ 公开项目证明：每个大于 2 的偶数 N 都可写成 N=a+b，其中 a、b 的 Liouville 函数值都为 -1。仓库给出论文、最终 Lean theorem、固定 Lean/mathlib 版本，以及 build、axiom 和 proof-route audit；另有独立 Linux replay。该结论是经典二元 Goldbach 的 Liouville 类比，并不是经典 Goldbach 猜想本身。
数学发现
推荐理由：它同时具备新的数论结果、完整 Lean 形式化与可复现验证记录；但公开材料不足以独立分离 GPT-6 Astra 与人类在选题、提示、编辑、形式化修复中的精确贡献，因此只记录公开归因，不进一步推断 AI 独立性。
00:14
arXiv / Axiom Math 精选 AI 评分 94 ☆ Ken Ono 与 Ashvin Swaminathan 证明 Browning–Sawin 关于随机符号系数超曲面的猜想：对固定 n，n+1 个变量、次数 d、系数独立均匀取 ±1 的齐次多项式定义奇异复超曲面的概率为 O_n(d^{-1/2})，正维奇异 locus 的概率指数小；当 n≥3 时，绝对不可约性失败也满足指数小概率。论文摘要同时说明这些结果已由 AxiomProver 在 Lean 中形式化，但形式化以已有文献为输入。
数学发现
推荐理由：这是新的代数几何/概率结果与 AI-assisted formalization 的组合案例；Radar 明确保留 formal certificate 的条件性，不把“assuming existing literature”的 Lean 证明描述成从基础公理完全闭合。
9月16日 ⌄ 星期三 · 1 条
08:00
Epoch AI 在 9 月 16 日更新 FrontierMath Open Problems 的归类政策：此前只有“AI 自主解决”才标为 AI，其他人机协作结果会被归到 human；新政策新增 human + AI 状态，用于人类主动指导 AI、但问题很可能没有 AI 就无法解决的情形。Epoch 同时把若干既有问题重新标记，并建议在必须做 human-vs-AI 二分分析时把这些结果视为 AI solutions。
工具与生态
推荐理由：随着 AI 参与数学发现从工具辅助走向深度协作，单纯 human/AI 二分已经无法准确表达贡献边界。这个 policy change 直接影响 benchmark 统计、AI 能力叙事、priority 与 attribution，是 AI4Math 评价基础设施的重要制度信号。
9月15日 ⌄ 星期二 · 3 条
11:20
lean-eval / Lean 精选 AI 评分 89 ☆ lean-eval 公共 results store 记录，NEAR AI w/ DeepSeek V4 在 9 月 15 日连续新增 13 个 accepted results，覆盖 Hadwiger、Szemerédi theorem、随机 Bernoulli 矩阵奇异性、Lorentzian polynomials、periodic tiling、Hessian estimates、Schmidt subspace、van der Waerden 等 formalization targets。记录保留 benchmark commit、accepted_at 与固定 submission ref，但当时 submission repository 为 private，因此外部只能核验 acceptance metadata，不能检查完整 proof source。
形式化数学
推荐理由：单日跨多个高难 formalization target 的 accepted burst 是模型+agent formalization capability 的清晰公开信号，尤其包含此前尚未在主流 proof assistant 中完成的 Szemerédi theorem target；但源码当时未公开，因此 Radar 只记录 leaderboard acceptance，不把它升级成可独立复现的公开证明包。
08:00
SAIR / Lean FRO 精选 AI 评分 90 ☆ SAIR Foundation 与 Lean FRO 在 9 月 15 日正式启动 Lean Kernel Challenge Stage 1，由 Joachim Breitner、Leonardo de Moura、Kim Morrison 与 Terence Tao 共同组织。比赛围绕 Lean 4 kernel 中 verified computation 的性能优化设置八个初始问题，参赛者提交优化实现及机器检查的正确性证明；赛后结果和 benchmark 数据计划以开源方式公开。
工具与生态
推荐理由：这不是普通编程竞赛，而是直接围绕 formal proof trust base 的可验证性能工程：要求优化 Lean kernel 计算同时提交机器可检验的正确性证据，对大规模 AI-generated proofs 的验证成本和 proof-checking infrastructure 都有直接意义。
01:58
arXiv / Google Research 精选 AI 评分 93 ☆ Stellar Colosseum 于 9 月 14 日首发，是一个 model-agnostic many-agent harness，面向数学和理论计算机科学中的 long-horizon research。系统先并行探索不同策略，用 readiness gate 判断何时进入分解，把 proof plan 表示成相互依赖的 section-level subproblems，再通过 targeted falsification 与 verifier feedback 把问题路由回相关论证节点。作者报告 Colosseum 在 TCS-Bench 上达到 71.0%，并在若干来自 FOCS/JMLR 的开放问题上得到新结果。
定理证明
推荐理由：它把 research-agent orchestration 从简单并行采样推进到显式的 strategy exploration、readiness gating、dependency-aware decomposition、targeted falsification 和 verifier repair loop，是 production-grade long-horizon mathematical research agent 的代表性架构信号。
9月14日 ⌄ 星期一 · 4 条
08:00
NYU Courant 介绍 Tristan Buckmaster 与 Levent Alpöge 的结果：他们构造了从光滑有限能量数据出发、受时空光滑外力驱动并在有限时间失去正则性的三维不可压 Euler 解；相关工作使用 Claude、Codex 等 AI 工具辅助，并将结果形式化、由 Lean 检查。该结果不同于 OpenAI 同期公布的 Navier–Stokes 主张。
数学发现
推荐理由：这是 AI-assisted research mathematics 与 formal verification 同时进入前沿 PDE 研究的强案例，并且研究对象、作者与 OpenAI 的 Navier–Stokes 项目不同，应作为独立事件保留。
08:00
Lean 4.34.0 于 9 月 14 日发布。官方 release notes 将 kernel reinforcement 列为本次重点：3 个 soundness issues 由 AI adversarial testing 发现并得到修复，同时加入一系列额外 defensive checks。该版本还改进 bv_decide、grind、floating-point API、linters 与 Lake，但对 AI4Math 最关键的是 proof assistant trust base 本身开始接受系统化 AI 对抗测试。
工具与生态
推荐理由：AI4Math 规模化后，关键问题不只是谁能生成更多 Lean proofs，而是 kernel 能否承受更强模型的 adversarial pressure。Lean 官方明确把 AI 测试发现的 soundness issues 纳入 release hardening，使这条事件直接关系到整个 formal-math verification stack 的可信度。
08:00
Boon Suan Ho · GitHub 精选 AI 评分 99 ☆ Boon Suan Ho 于 9 月 14 日公开 Nivat conjecture 的 Lean 4 + mathlib formalization，并明确声明完整证明由 GPT-6 Pro 在其 prompts 下生成，论文文本由 AI 起草，Lean formalization 与文档由 GPT-6 Astra Ultra through Codex 生成。仓库将 Challenge.lean 与 Solution.lean 分离，并登记 Palomar；公开验证记录包括 Lean build、Comparator 与 NanoDa 检查。维护者同时明确表示自己不是该领域专家，也没有真正 digest 这份证明。
数学发现
推荐理由：这是 AI4Math provenance 与 verification 边界极具代表性的事件：模型被直接归因为开放猜想的 proof generator，并有 machine-checked formal artifact；但 human mathematical digestion 和 specialist peer review 尚未完成，因此 Radar 只记录为公开 claim + formal verification，不自行宣布学界最终解决。
03:19
Michael Mazur / Palomar 精选 AI 评分 92 ☆ Michael Mazur 9 月 13 日发布 Dimitrov Conjectures 1 和 3 的 Lean 4 形式化。公开仓库称 OpenAI Codex 在其指导下承担了 substantive target selection、proof discovery、literature searching、Lean formalization 与 documentation。形式化覆盖所有自然数 k≥1、n≥2，并给出 equality iff n is prime；`Solution.lean` 无 sorry 或 custom axiom，仓库提供 `lake build`、`--trust=0`、Comparator 与 NanoDa replay。项目同时明确不声称历史首证，priority 尚未获得源论文作者或独立专家确认。
形式化数学
推荐理由：这条同时具备 AI 参与 proof discovery、完整 Lean artifact 与多层 verification surface，而且项目主动限制 novelty/priority claim；它非常适合作为‘机器验证成立’与‘历史原创性尚未确认’可以同时成立的 AI4Math 案例。
9月13日 ⌄ 星期日 · 2 条
22:10
Ning Wang 等人在 9 月 13 日首发论文，报告在 fully programmable superconducting quantum processor 上实验实现 automated geometry theorem proving。第一套框架把 Wu 代数消元法改写为 quantum pseudo-division，并把多元多项式编码进 superposition states；第二套框架把 full-angle method 表述成 hybrid quantum strategy-guided backward symbolic reasoning。作者以正方形对角线垂直和一道 1978 IMO 几何题为示例，在真实超导处理器上完成证明。
定理证明
推荐理由：它不是把量子硬件当普通 benchmark accelerator，而是把 algebraic elimination 与 backward proof search 明确映射到量子/混合执行路径，首次把 automated geometry proving 作为 near-term quantum processor 上的实验任务公开展示。
07:38
Romain Popescu 证明 Caragiu、Vicol 与 Zaki 关于 Conway subprime closure 的增长猜想：由 C₀={1} 且 Cₙ₊₁=Cₙ∪(Cₙ∘Cₙ) 定义的集合满足 |Cₙ₊₁|/|Cₙ|→(1+√5)/2。论文摘要明确说明底层数学证明在 GPT-6 Astra 的算法辅助下构造，并使用 Lean 4 对正确性进行了形式验证。
数学发现
推荐理由：这条同时满足‘新数学结果 + 明确 AI 参与 proof construction + Lean machine verification’三项高价值条件。Radar 只据作者公开说明记录 GPT-6 Astra 的算法辅助，不把它扩写为自治证明发现。
9月12日 ⌄ 星期六 · 4 条
14:09
Jit Wu Yap 基于 Xie–Yang 通过有限域上的 Tate 定理重新证明 Faltings isogeny theorem 的思路，进一步证明：有限域上 isogeny class 的有限性可推出数域上的有限性，从而得到 Shafarevich 猜想的一个新证明。论文摘要明确写道，这一证明是通过使用 GPT-6 Astra Ultra 获得的。
数学发现
推荐理由：作者把研究级数论/算术几何证明的获得过程直接归因于 GPT-6 Astra Ultra，AI 参与程度显著高于普通写作辅助。不过公开摘要没有提供 Lean certificate 或独立专家复核，因此 Radar 保留为‘作者归因的新证明’，不把可信度提升到机器验证层级。
09:31
Angel Ivanov Raychev 对从单个方格向四个方向添加直臂得到的 polyomino 进行完整分类，覆盖 rectangle、half-strip、bent strip、quadrant、strip、half-plane、plane 以及 rep-tiling 能力。论文把周期构造、几何 obstruction 与有限 symbolic certificates 结合起来，并给出覆盖所有自然数四元组的 Lean 4 development；摘要同时记录后续 proof development 与 formalization 使用了 AI 辅助。
形式化数学
推荐理由：完整参数空间分类、可机器检查的 Lean artifact 与明确记录的 AI-assisted proof development 共同构成了强 AI4Math 信号；相比只对个别 finite cases 做验证，这里的 formalization 直接覆盖任意自然数臂长及无限 tiling 语义。
01:18
中关村人工智能研究院等团队发布 ZGCM-1，一个从零训练的 7.39B dense foundation model，面向 mathematical reasoning 与 tool-assisted agentic search。系统支持 256K context，结合 hybrid attention、FP8 Muon、progressive long-context mid-training，以及把交互轨迹重构为 MDP 的训练流程。论文还描述 agent swarms 参与 cluster operations、data curation 与快速诊断评测；项目公开 pre-/mid-/post-training weights、中间 checkpoints、训练代码、分阶段数据与 recipes 以及 W&B logs。
数学推理
推荐理由：ZGCM-1 的价值不只是又一个声称数学能力更强的模型，而是把数学推理、外部搜索、长上下文与 agentic training 放进一个近乎全开放的复现面，并公开从数据到训练日志的完整资产；这使其具备明显高于普通 benchmark model release 的研究可用性。
00:00
SAIR / Caltech Math-AI 精选 AI 评分 92 ☆ SAIR Foundation 与 Caltech Math-AI group 于 9 月 11 日启动 Andrews–Curtis Conjecture Challenge，由 Sergei Gukov、Terence Tao 与 Lucas Fagan 组织。挑战围绕 Andrews–Curtis conjecture 及其 stable version 设置可检查的 combinatorial search / proof tracks，目标包括寻找 balanced group presentations 的短 trivializations、推进经典候选反例以及最终证明或否证猜想。该问题与低维拓扑、光滑四维 Poincaré 猜想等方向相关，并因解答可通过明确的 move sequence 与 verifier 检查而适合 AI search。
工具与生态
推荐理由：这不是普通数学竞赛，而是把著名开放问题重构为具有显式 action space、可重放 candidate solution 与 verifier 的 AI/search research environment；对研究 AI-driven mathematical discovery、RL/combinatorial search 与可验证开放问题 benchmark 具有直接价值。
9月11日 ⌄ 星期五 · 2 条
08:00
Terence Tao / Math & AI 精选 AI 评分 94 ☆ Terence Tao 等 25 位菲尔兹奖得主于 9 月 11 日联合发布声明，讨论 AI 公司将解决著名数学问题作为能力 benchmark 可能带来的研究目标错位。声明并不否认 AI 对数学研究的潜在价值，而是强调 conceptual understanding、公开交流、正确归属、学生培养与数学知识长期传承等目标不应被单纯的“解题速度”替代，并呼吁数学共同体与 AI 开发机构共同处理这些治理问题。
工具与生态
推荐理由：这是一项直接影响 AI4Math 研究规范与治理的领域级事件：25 位菲尔兹奖得主围绕 benchmark incentives、理解、归属和知识传承形成公开共同体立场，并在后续机构回应中成为引用基准。Radar 将其作为 ecosystem / governance signal 收录，而不是把声明中的规范性判断当作已证明事实。
04:23
arXiv / GitHub 精选 AI 评分 91 ☆ Ziang Li 与 Yusheng Luo 发布 Sullivan No Wandering Domains theorem 的 Lean 4 形式化：次数至少为 2 的 Riemann sphere 有理自映射，其每个 Fatou component 最终都会周期化。项目同时形式化 normal families、Montel–Carathéodory theorem、Julia/Fatou sets、Sobolev regularity、Cauchy/Beurling transforms、quasiconformal equivalence 与 measurable Riemann mapping theorem 等大量基础。公开仓库说明总体架构和核心 theorem statements 由人类设计与核验，Claude agents 辅助 individual proofs 与 boilerplate；项目无 sorry 或新增 axiom。
形式化数学
推荐理由：这是一项覆盖复动力系统与 quasiconformal analysis 大量深层基础设施的 substantial formalization，而不是少数独立定理的机械翻译；其公开 AI disclosure 也清楚区分 human architecture / statement verification 与 agent-assisted proof coding，因此具有较高的 AI-assisted formal mathematics 方法学价值。
9月10日 ⌄ 星期四 · 2 条
17:48
Magenta 是一个 training-free agentic pipeline：从自然语言数学题出发，先给出解答，再生成 Lean 4 statement 与 machine-checked proof。系统额外加入 statement judge，检查形式化陈述是否忠实保留原题语义；当证明失败时，error-attribution judge 判断问题应回到数学重新推导，还是进入局部 Lean repair。论文报告其在所评测的 olympiad benchmarks 上达到 100% accuracy，并在搭配 K2-Horizon-7B 时解决全部 6 道 IMO 2026 题。
定理证明
推荐理由：其关键贡献不是单纯提高 solve rate，而是把 informal reasoning、autoformalization、statement fidelity verification 与 Lean feedback repair 组成一个闭环，并直接针对‘错误 statement 也能被形式证明’这一 AI4Math 可靠性失败模式设计防线。
01:07
Marc Kegel、Shana Yunsheng Li 与 Qiuyu Ren 构造出一个具有不可解 word problem 的 3-generator 9-relator group，并据此得到两个 fixed-size Adian–Rabin families：4 generators / 11 relators 与 2 generators / 10 relators；进一步推出 #7(S²×S²) 在拓扑意义下不可识别、#9(S²×S²) 在光滑意义下不可识别，改进此前已知界。arXiv comment 明确写明 main results were developed by ChatGPT 5.6 Sol；论文同时给出代数结果的 Lean 4 machine-checked formalization。
数学发现
推荐理由：这条同时具备新的群论/几何拓扑结果、作者对 ChatGPT 5.6 Sol 的明确核心贡献披露，以及 Lean 4 对主要代数结果的机器验证，是高度典型的 AI-led research mathematics 案例。Radar 只记录作者披露与 formal artifact 所支持的贡献边界，不把四维流形后果描述成已被 Lean 全部形式化。
9月9日 ⌄ 星期三 · 1 条
01:59
StochBench 提出 450 道 graduate-level stochastic-processes Lean 4 problems，每题与自然语言原题配对，覆盖有限与可数 Markov chains、renewal processes、random walks、martingales、stopping times、queues、Brownian motion、stochastic calculus、weak convergence、Poisson 与 continuous-time Markov processes。论文报告 Opus 4.8-based proof agent 在每题 15 分钟预算下解决 157/450（34.9%），并公开 benchmark dataset 供 proof generation 与 autoformalization 研究使用。
评测与数据
推荐理由：它补上现有 Lean/LLM benchmarks 偏重 olympiad / competition math 的结构性缺口，把 formal theorem proving evaluation 扩展到研究生级随机过程这一应用数学域，并提供 natural-language / Lean 配对与可复用公开数据集，因此具有明确的评测基础设施价值。
9月8日 ⌄ 星期二 · 2 条
08:00
OpenAI 公布一份由内部 AI 系统生成的 Navier–Stokes 证明与 Lean 形式化，并表示该构造给出了平滑外力下有限时间奇性，对应 Clay 问题表述中的 breakdown alternatives C/D。OpenAI 还披露相关搜索由大规模协同 agents 完成。Radar 将其记录为 OpenAI 已公开的研究主张与形式化产物，而不是替代数学共同体的最终独立认证。
数学发现
推荐理由：这是 AI 直接参与高影响开放数学问题求解并同时公开 Lean 形式化的标志性事件；结论强度极高，因此措辞必须保持为“OpenAI 公布并主张解决”，而非由 Radar 自行宣布最终定论。
05:31
arXiv / GitHub 精选 AI 评分 98 ☆ Tom Adamczewski、Bernhard Böhmler 与 René Marczinzik 于 9 月 7 日公开论文，构造 Köthe 猜想的反例，并据此否定回答 Louis Rowen 的一个 1989 年问题。配套公开仓库说明，最初 matrix-form counterexample 与 Lean 4 proof 由预发布 GPT-6 Astra 在 Epoch AI 的 LeanOpenProblems autonomous evaluation 中独立产生；随后作者对 AI 结果进行数学检查，并把构造推广到任意可数域，写成对 Köthe 原始猜想的直接反例。
数学发现
推荐理由：这条把 autonomous AI discovery、Lean machine checking、human specialist review 与后续 mathematical generalization 连成完整 provenance chain。Radar 将 9 月 7 日记录为论文公开与人类核验/推广事件；最初 GPT-6 Astra discovery 本身发生在更早的 9 月 3 日，因此不重写其原始发现日期。
9月7日 ⌄ 星期一 · 1 条
11:46
Shengtao Guo、Ethan X. Fang 与 Junwei Lu 证明经典 complex Grothendieck constant 满足 K_G^C > 1.35584631827168，相比 Davie 的经典下界显著推进，并关闭 Davie 下界与 Haagerup 上界之间超过四分之一的缺口。论文明确写明 lower bound 与 proof 由 Odin Automatic AI Research Agent 发现；最终数值不等式通过 interval arithmetic 严格认证，并随论文提供可执行 verification artifacts。
数学发现
推荐理由：这是明确的 AI-led research mathematics：论文直接把新下界与证明发现归因于 autonomous research agent，同时提供严格数值证书和可复用 verification artifacts。Radar 不把该结果描述为求出了 complex Grothendieck constant 的精确值；它只是显著推进已知下界。
9月6日 ⌄ 星期日 · 2 条
08:00
Lech Mazur 证明：对任意固定正整数目标 a 且 3∤a，普通 Collatz 迭代中最终到达 a 的正整数集合具有正下自然密度。ProofAtlas 明确记录 OpenAI Codex 对 computation、proof strategy、formalization 与 exposition 有 substantial contribution；公开 Lean artifact 通过 build，三个主定理根无 unfinished proof。结果还推出：若存在一个正整数永不到 1，则不收敛集合具有正下密度；而 upper-natural-density-one convergence 会推出所有正整数最终到达 1。后者的 density-one 前提并未被证明。
数学发现
推荐理由：这条同时具备研究级数论/动力系统结果、明确 AI 实质参与和 Lean machine checking。其价值也在于边界写得非常清楚：它显著加强 Collatz predecessor 的密度结果，但没有证明 full Collatz conjecture，也没有证明 density-one convergence 前提。
08:00
Palomar / aiXiv 精选 AI 评分 92 ☆ Ralf Stephan 发布针对 Bugeaud Problem 10.61 的 Lean 4 / Mathlib development。公开记录明确写明数学与 Lean 文本由 agents 产生：Fable-5 agent 撰写数学笔记，Opus-5 agent 完成形式化，作者负责选题、逐轮引导与筛选结果。项目把问题转化为 symbolic-dynamics、pressure 与 covering certificates，并在 α=2+√5 和 α=2+√3 两个 quadratic Pisot 情形真正推出非均匀分布结论；一般问题及超出该 covering range 的 quadratic cases 仍保持开放。
形式化数学
推荐理由：它不是简单把已有论文翻译成 Lean，而是由 AI agents 直接发展数学 criteria 与 formal certificate machinery，并把开放问题推进到两个可完全机检的具体情形。Radar 保留其严格边界：一般 Bugeaud Problem 10.61 并未解决，且作者本人明确没有独立验证 informal-to-formal fidelity。
9月5日 ⌄ 星期六 · 1 条
20:11
Ioannis Tzachristas 证明：若紧集 K⊂ℂ 的 logarithmic capacity 等于 1，则允许任意次数与重根时，以 K 中点为零点的 monic polynomials 的 unit lemniscates 面积下确界为 0。结合既有 capacity>1 结果与非有界闭集的补充论证，这给出 transfinite diameter 至少为 1 的任意无限闭集上的 vanishing 结论，从而回答 Erdős Problem #1040 的相关问题。论文明确声明该结果通过作者使用 OpenAI GPT-6 Astra（经 Codex）的 prompting strategy 获得，AI 参与 proof exploration、mathematical reasoning、literature checks、manuscript drafting 与 parallel internal reviews。
数学发现
推荐理由：这是研究级开放问题的 AI-assisted mathematical discovery，且作者对 AI 的数学推理角色有明确披露。与此同时，当前公开材料没有 Lean certificate、独立专家验证或同行评审，因此 Radar 保留为作者公开的 preprint-level proposed result，而不升级为已独立确认的最终数学结论。
9月4日 ⌄ 星期五 · 2 条
08:00
Anthropic 宣布公开费马大定理的首个完整 computer-checked proof，并称 Claude 在 11 天内 largely autonomously 将相关现代证明形式化为 Lean。该事件的核心是把一个大型、成熟的人类数学证明转化为可由 proof assistant kernel 检查的形式资产，而不是提出新的费马大定理证明。
形式化数学
推荐理由：经典重大定理的大规模自动形式化是 AI4Math 的关键能力边界；这里有公开的一手机构说明和明确的 machine-checked 目标，且应与“AI 发现了 FLT 新证明”严格区分。
08:00
数学家 Djalil Chafaï 报告使用 ChatGPT Codex CLI（5.6 Sol）和 agents，将其最新论文 arXiv:2608.19358v2 的 Theorem 1.9 自动形式化为约 16,400 行 Lean、约 75 个文件。整个过程在个人 Debian 工作站上耗时约 5 小时 48 分钟、使用约 806 万 tokens；最终 full make 成功，没有 sorry、admit、sorryAx 或 project axioms，主定理仅依赖 Mathlib 标准公理。
形式化数学
推荐理由：这条的重要性不在于提出新的前沿数学结果，而在于把 AI-assisted formalization 从 frontier-lab mega-project 下沉到普通研究者的单机工作流：真实论文定理、agent orchestration、完整 Lean artifact、axiom audit 和可复现 build 在约 6 小时内闭环。它为 AI4Math 的个人研究基础设施提供了很强的工程信号。
9月3日 ⌄ 星期四 · 8 条
15:35
AutoGraphForge 报告了一个自动图论研究 pipeline：生成猜想后以反例扩充图数据，使用经典关系 novelty filter、约 34.8 万个图的测试集和主动反例搜索进行筛选，再将候选确定性转换为 Lean 4 statement skeleton，并接入 DeepSeek-Prover-V2-671B 与 OProver-32B，在 Lean kernel 下独立验证。作者报告多轮运行得到 6,522 个经当前反驳流程存活的猜想。
数学发现
推荐理由：它把 conjecture generation、novelty filtering、counterexample search 和 formal verification 连成端到端研究流程，比单纯数学 benchmark 刷分更接近自动数学发现系统。
08:00
LeanOpenProblems / GitHub 精选 AI 评分 99 ☆ Epoch AI 的 LeanOpenProblems evaluation 中，一个预发布 GPT-6 Astra agent 在无人查看或引导 proof search 的条件下，对 Formal Conjectures 中 Köthe 猜想的 Krempa matrix formulation 进行单次自主尝试，找到一个反例并提交 Lean 4 证明。最终 Spec.lean 在独立 pristine container 中由 Comparator 检查与 trusted statement 完全一致，并只允许标准逻辑公理。该原始构造后来由 Adamczewski、Böhmler 与 Marczinzik 做数学检查和推广，并在 9 月 7 日形成更一般的人类论文。
数学发现
推荐理由：这是极强的 autonomous AI mathematics provenance：开放研究问题、无人工 steering、单次 agent run、Lean kernel / Comparator 检查，并且后续出现了数学家独立消化与推广的论文链条。Radar 将这里记录为原始 autonomous discovery；9 月 7 日的人类论文作为同一 story 的后续验证与推广单独保留。
08:00
Epoch AI 在 9 月 3 日的 GPT-6 Astra pre-release evaluation 更新中报告：FrontierMath Erdős 由 68 个截至 2026 年 8 月仍开放、并形式化为 Lean 的 Erdős 问题组成；每题一次尝试、预算 $300 与 72 小时 working time，只有通过 Comparator / Lean kernel 的 proof 或 disproof 才计为解决。预发布 GPT-6 Astra 在正式 protocol 下解决 2/68：对 problem 74 找到反例，并证明 problem 126；GPT-5.6 Sol、GPT-5.5、Claude Fable 5.1 与 Claude Fable 5 均为 0。另有 larger-budget 非标准尝试解决更多问题，但不计入 3% benchmark score。
评测与数据
推荐理由：这是少见的开放研究数学 fixed-budget benchmark milestone：评价对象不是竞赛题，而是如果由人类解决会达到高水平论文价值的开放问题，并用 Lean / Comparator 给出确定性成功标准。Radar 严格保持 benchmark 与额外 inference-scaling attempts 的边界，不把后者计入 3% 分数。
06:29
Sean N. Curry 构造一个 strongly pseudoconvex CR 3-manifold：它的 canonical bundle 具有 nowhere-zero closed section，却仍不能局部嵌入 ℂ²，从而给出 Trautman conjecture 的 smooth counterexample。作者在 acknowledgements 中说明，counterexample construction 是在 8 月 18 日通过与 ChatGPT Plus 的实验发现的；ChatGPT 还用于初稿和 proofreading。作者随后独立检查全部计算与论证，并对论文正确性负责。
数学发现
推荐理由：这是一条清晰的 AI-assisted counterexample discovery：作者明确说反例构造通过 ChatGPT 实验获得，并自行完成数学核验。由于论文仍标为 preliminary version，且没有 formal artifact 或独立外部复核，Radar 不把它提升为 machine-verified / independently corroborated 级别。
06:06
Carnegie Mellon University / Wesley Pegden 精选 AI 评分 97 ☆ Wesley Pegden 宣布 Trellis 完成 Strong Perfect Graph Theorem 及其完整 Berge-graph decomposition theorem 的端到端 Lean 形式化。CMU 项目页记录：该 run 从 7 月 17 日持续到 9 月 1 日，约 1,460 个 supervisor cycles，最终接近 1,500 个 nodes、约 1,100 个 theorem-like statements、390 个 definitions、约 530,000 行 Lean。除 source manuscripts 与中途对 statement shapes 的人工确认外，没有提供数学内容、proof steps 或 Lean hints；所有 obligations 都在 isolated checker 中构建，无 sorry，且只使用标准公理。
形式化数学
推荐理由：这是大型自动形式化工程的能力边界事件：一个高度复杂、长篇的人类数学证明被 agentic workflow 端到端转化为可由 Lean kernel 检查的形式资产，同时把 human intervention 压缩到 statement-shape ratification。Radar 保留关键边界：Lean 检查 proof terms，而原论文与形式化 statements 的语义对应仍需要人类承担责任。
04:53
OpenAI · GitHub 精选 AI 评分 92 ☆ OpenAI 公开了素数间隔上界 186 的 Lean 4 形式化与 Python 数值证书。仓库明确说明 Lean 结果仍依赖 3 个显式输入公理，数值估计也尚未全部转化为 Lean 证明；项目 metadata 记录了 GPT-6 Astra / Codex agent 参与、Comparator、Nanoda 与 Lean kernel 检查。
形式化数学
推荐理由：价值不只在结论本身，更在于它把 AI-assisted formalization 的证明边界、未证明输入和机器检查状态公开写进 metadata，适合作为可审计形式数学工作流案例。
02:59
Kada Williams 公布对 1983 年 Daykin–Frankl conjecture 的证明：若 P 是 Boolean lattice Q_n 的 convex subset，则 P 至少包含 |P|·binom(n,⌊n/2⌋)·2^{-n} 个两两不可比较元素。论文摘要直接说明其工作是“verify and communicate an LLM-generated proof”，公开记录将模型标为 GPT-5.6 Sol Pro。论证实际上证明一个更强的 product-width inequality，并以 k=0 推出原猜想。
数学发现
推荐理由：作者明确把核心证明来源归于语言模型，并在公开论文中自行核验和传播结果，因此 AI 的数学推理角色是实质性的。当前没有 Lean formalization 或独立专家复核，Radar 因而保持为 author-verified preprint claim，而不是机器验证的最终结论。
01:50
Bostanci、Grewal、Haferkamp、Huang、Hwang、Natarajan 与 Nirkhe 构造一个 quantum oracle，使得 QMA^U ≠ QMA(2)^U；作为非 oracle 后果，他们证明在 ε+δ<1 时任何 (ε,δ)-disentangler 都需要随输出 qubits 指数增长的输入规模，从而解决 Watrous 的 no-disentanglers conjecture。作者披露主定理的 proof idea 由 ChatGPT 5.6 Sol 在被引导到 She–Yuen polynomial method 后提出，随后由人类作者验证、简化并发展为论文。
数学发现
推荐理由：这是 theoretical CS / quantum complexity 中 AI 直接参与核心证明思路发现的强案例，并有明确人类后续验证与发展链条。Radar 保留其 relativization 边界：结果给出 quantum-oracle separation，不等于无条件证明 QMA(2)≠QMA；公开材料也没有 formal proof 或独立复核。
9月1日 ⌄ 星期二 · 1 条
08:00
Epoch AI 于 9 月 1 日正式发布 FrontierMath Erdős，由 Thomas Bloom 参与筛选 68 个截至 2026 年 8 月仍开放、具有较高数学意义和难度的 Erdős 问题。所有题目都被形式化为 Lean statement，AI 系统必须在固定预算内提交完整 Lean proof 或 disproof 才算解决；公开 benchmark 页面同时提供 methodology、Lean statements 与 evaluation scaffold，以改善此前开放数学问题评测中存在的 curation、verification 与 replicability 问题。
评测与数据
推荐理由：它把真正仍开放的研究数学问题变成可重复、固定预算、Lean-kernel-checkable 的 model evaluation surface，显著提高 AI 解开放数学问题时的可比较性与证据质量。Radar 将其作为 benchmark launch 收录，并与 9 月 3 日 GPT-6 Astra 在该 benchmark 上取得 2/68 的模型成绩更新严格区分。
8月20日 ⌄ 星期四 · 1 条
01:19
Jihao Liu 构造一个 polarized smooth projective fivefold，证明它 K-polystable 但不存在 constant scalar curvature Kähler metric，从而否定 cscK 版本的 Yau–Tian–Donaldson conjecture。论文摘要明确写明 main result 使用 generative AI 获得，特别包括 GPT-5.6 Sol、Fable 5 与 Danus system，并在 appendix 中提供与 Bin Dong、Guoxiong Gao 合写的 AI-use report。
数学发现
推荐理由：这是高层代数/微分几何中模型直接参与 main result discovery 的强事件，而且论文主动附上 AI provenance report。Radar 仍按 preprint 级别记录，不将其写成已经完成独立同行评审的最终社区共识。
8月18日 ⌄ 星期二 · 1 条
08:00
Terence Tao / Palomar 精选 AI 评分 95 ☆ Terence Tao 于 8 月 18 日宣布 Palomar registry 正式开放 submissions。项目针对 AI-generated / AI-assisted proofs 大量涌现后出现的 trust problem：不仅检查 Lean repository 是否 typecheck，还检查是否引入额外 axioms、exact formal statement 是什么，以及 formal statement 与 informal claim 的语义对应。Palomar 由 Lean FRO 与 ICARM 孵化，定位类似形式数学的 public registry，而不是 novelty 或 mathematical importance 的自动认证。
工具与生态
推荐理由：随着 AI 产生的 formal proofs 数量上升，trust bottleneck 从‘有没有 Lean proof’转移到‘statement 是否一致、有没有隐藏 assumptions、来源是否可审计’。Palomar 直接为这个 production verification layer 建立公共基础设施。
8月16日 ⌄ 星期日 · 1 条
08:00
Lech Mazur 发布 Bondy 1980 minimum-degree longest-cycle conjecture 的 proof candidate。GPT-5.6 Pro 参与 computation、proof strategy、gap discovery、formalization 与 exposition；一个 204-module、约 10 万行的 first-party Lean cone 检查精确 theorem `Bondy.bondy_longest_cycle`，无 unfinished proof。ProofAtlas 同时明确：paper-to-formal-statement alignment、specialist peer review、unrelated replication 与 historical priority 仍未完成。
形式化数学
推荐理由：这是长程 AI-assisted graph-theory proof development 与 substantial Lean artifact 结合的代表案例。现有证据强在 exact endpoint machine checking，弱在 informal paper 与 formal theorem 的独立语义对齐，因此保持 candidate 状态。
8月14日 ⌄ 星期五 · 1 条
08:00
Lech Mazur 发布一个从 11×8 rectangle 经 30 步合法交替 moves 到达的 28-cell Domineering position，其 exact game 为 {17/8 | -2+*}、temperature 33/16>2，从而给出 Berlekamp temperature-2 conjecture 的 counterexample candidate。GPT-5.6 Pro 参与 mathematical exploration、exact computation 与 adversarial auditing；Lean 检查完整 move replay、game equivalence、thermograph 与 existential witness，但 specialist review 和 unrelated replication 当时仍开放。
形式化数学
推荐理由：它展示 finite combinatorial-game witness 如何被 AI 搜索、exact computation 与 Lean certificate 共同锁定。Radar 保留其 scoped formalization 与 review-pending 边界，不把有限 witness 之外的更广泛 thermograph claims 一并视作正式验证。
8月12日 ⌄ 星期三 · 1 条
08:00
Epoch AI / GitHub 精选 AI 评分 90 ☆ Levent Alpöge、Philippe Voinov 与 Saul Reynolds-Haertle 在使用 Claude 的协作中公布 order 668 Hadamard matrix construction。Epoch AI 于 8 月 12 日把该 FrontierMath Open Problem 暂标为 solved by AI，并明确说明 attribution 仍可能调整。随后公开 decoder / payload 被独立重建，668×668 ±1 matrix 的所有不同行内积均精确为 0；这解决的是 order 668 这个具体存在性问题，不是一般 Hadamard conjecture。
数学发现
推荐理由：有限构造可被完全精确验证，且直接解决此前最小未决 order 之一；但 Claude 与三位人类的核心贡献边界并不清楚，Epoch 的 AI attribution 当时也明确是 provisional，因此 Radar 不升级为 autonomous-AI solve。
8月10日 ⌄ 星期一 · 1 条
08:00
Anthropic 报告，一个未发布 research version of Claude 在尝试 Riemann hypothesis 时没有解决 RH 本身，却结合 Aryan、Baluyot–Goldston–Suriajaya–Turnage-Butterbaugh 与 Bombieri 的既有工作，把可证明位于 critical line 上的 zeta zeros 比例下界从 41.6% 提升到 67.2%。约 60 个 Claude subagents 在一天半内协作，Anthropic 数学家 Levent Alpöge 与 Ralph Furman 检查结果；Claude 还协助生成通过 Comparator 的 Lean formalization。
数学发现
推荐理由：这是 autonomous/agentic math research 的强案例：开放式目标、数十 agents 的长程探索、意外产生新的 number-theory bound，并附人类数学家检查和 Lean formalization。Radar 明确写清它没有证明 Riemann hypothesis。
8月8日 ⌄ 星期六 · 1 条
15:32
Bryce Putman 给出一个 112 顶点 simple bridgeless cubic graph，没有 Petersen coloring，也没有 normal 5-edge-coloring；论文公开图的 SHA-256、SAT encodings、CaDiCaL UNSAT 结果、DRAT proofs 与重建程序。论文的 computational provenance section 披露 OpenAI language-model systems 广泛参与 discovery、computational search、verification 与 preparation。次日 Jorik Jooken 又给出短的人类可检查证明。
数学发现
推荐理由：它将 AI-assisted combinatorial search 与完全显式的 finite witness、SAT/DRAT certificates 和后续 human-checkable proof 串成较完整的验证链。论文未给出具体 OpenAI model 或精确 credit split，因此 Radar 不推断更细的自治程度。
8月7日 ⌄ 星期五 · 1 条
01:01
Emiel Lorist、Martin Meyries 与 Mark Veraar 对 Hilbert 空间 inverse generator problem 给出否定答案，并从同一有限维构造导出 ordinary 与 strong Kreiss 条件之间的分离等结果。公开 tool disclosure 显示 GPT-5.6 Pro 用于探索 Schauder-basis counterexamples、辅助形成显式有限维构造与常数，Claude Fable 用于 Lean 4 formalization；机器形式化覆盖核心 finite-dimensional theorem，而非所有后续 semigroup / Kreiss 推论。
数学发现
推荐理由：这是 functional analysis 中 AI 参与核心 finite-dimensional construction search 的实例，且 formalization 明确覆盖核心 machinery。Radar 不把部分 Lean formalization扩大为整篇论文所有推论均已 machine-checked。
8月6日 ⌄ 星期四 · 1 条
01:46
Gonzalo Cao-Labora 与 Jaume de Dios Pont 构造无限多个非圆的平面光滑域，使其存在边界上为常数的 Neumann eigenfunction，从而否定平面 Schiffer conjecture，并通过经典等价关系否定相应 Pompeiu problem。公开披露显示模型参与数值探索、Bessel estimate proof drafts 与 exposition；GPT-5.6 从早期 manuscript 生成 Lean 4 formalization。作者自身提出并发展 bifurcation construction。
数学发现
推荐理由：这是经典 spectral geometry 开放问题被人机协作解决并配套 formal verification 的高价值事件。Radar 明确区分人类提出的新构造策略与模型在证明草稿、数值验证及形式化中的辅助角色。
8月5日 ⌄ 星期三 · 2 条
08:00
Lech Mazur 发布 Sendov conjecture 的 computer-assisted proof candidate 与完整 Lean package。ProofAtlas 记录 GPT-5.6 Pro 对 mathematical exploration、proof development、exact computational testing、adversarial auditing 与 exposition 有直接贡献；公开 Lean import closure 超过 92,000 行并成功检查 exact endpoint `Sendov.sendov_conjecture`。当前 manuscript-to-formal-statement alignment、specialist review 与 accepted-result review 仍未完成。
形式化数学
推荐理由：它把 AI-assisted proof development、exact certificates 与大规模 Lean checking 集成到一个可审计 package 中。由于独立 statement-alignment 与 specialist acceptance 当时仍开放，Radar 保留为 Lean-checked proof candidate，而非自行宣告 conjecture 已最终解决。
01:30
Wouter Cames van Batenburg 与 Samuel Korsky 证明对每个固定直径 k，最大度至多 d 的图最大阶数 n_k(d) 满足 n_k(d)/d^k→1，解决 Bollobás 的渐近 degree–diameter conjecture，并给出 edge variant 的相应结果。作者披露 GPT-5.6 Pro 在探索中提出把 complete flags 分成 odd/even-rank subflags 的关键构造想法；作者随后发展并验证论证，生成式 AI 也辅助了 Lean 4 formalization。
数学发现
推荐理由：它是 AI 提供核心 construction idea、数学家完成发展与验证、并进一步形成 Lean artifact 的清晰人机协作案例；同时真正解决一个 1978 年以来的渐近图论问题。
8月1日 ⌄ 星期六 · 1 条
08:00
OpenAI 于 8 月 1 日发布内部版本 Astra 产生的十项研究结果，覆盖高维 sphere packing、binary/spherical codes、non-sofic groups、Connes rigidity、arithmetic circuit complexity、quantum parallel repetition、closest vector problem、Ehrhart volume conjecture、multicolor Ramsey numbers 与 extremal graph theory。OpenAI 表示数学论证由系统生成，人类负责整理 manuscript 与正确性责任，随后模型为每项结果生成 Lean certificate；官方估算寻找这些解答所需 tokens 若按 Sol API 计费约为 2,000 美元。
数学发现
推荐理由：这是 2026 年 AI4Math 的标志性批量研究发布：不是单一 benchmark，而是十个长期开放或长期停滞问题上的新数学结果，并配套 Lean 证书与公开 provenance。Radar 将十项结果作为同一发布事件记录，避免人为拆成十条重复事件。
7月31日 ⌄ 星期五 · 1 条
08:00
Epoch AI 于 7 月 31 日将 FrontierMath: Open Problems 扩展到 50 个 significant unsolved research problems，并报告当时 AI 已解决 3 个。与此同时，项目因 verifier 无法以足够 fidelity 捕捉正确答案而移除两个问题，并因 notability 不达标移除一个 Ramsey-style hypergraph problem。这次更新把 benchmark curation 与 verifier reliability 明确提升为一等治理目标。
评测与数据
推荐理由：这不是普通 benchmark 扩容：Epoch 同时公开因为 verifier fidelity 与 problem notability 主动删题，体现 AI4Math evaluation 已开始把数据质量、可验证性与研究价值作为共同约束。
7月28日 ⌄ 星期二 · 2 条
18:20
Dominik Peters 证明 Kemeny rank aggregation 在只有 3 个 voters 时已经 NP-complete，回答 Dwork 等人 2001 年提出的问题。论文明确说明 reduction 在 2026 年 7 月由 GPT-5.6 Sol Ultra 找到，并部分由 Claude Fable 5 协助简化；最终 reduction 从 MAX CUT 出发，由作者整理和验证。
数学发现
推荐理由：这是 social choice / theoretical CS 中非常清晰的 AI-generated reduction discovery：核心 hardness construction 被作者直接归因给 frontier model，另有第二模型参与简化。
08:00
Epoch AI 于 7 月 28 日将 Q₂ absolute Galois group presentation 作为 FrontierMath: Open Problems 的第二个已解决问题公开确认。最早已知 verifier-accepted solution 来自 Claude Fable 5，由 David Roe 于 6 月 9 日 elicited；6 月 24 日又有 GPT-5.5 Pro solution。Epoch 明确说明 verifier 给出强证据，但当时仍需数学家确认 AI 是否真正能给出完整证明，因此 7 月事件代表 benchmark/public-confirmation milestone，而非把 6 月最初 generation 重新定日。
评测与数据
推荐理由：它是 FrontierMath Open Problems 从‘AI 可能做出研究贡献’转向‘公开可验证开放问题被模型实际攻破’的关键里程碑，同时很好展示 verifier acceptance 与 full-proof / human confirmation 之间的证据差异。
7月27日 ⌄ 星期一 · 1 条
23:07
Zipei Nie 与 Jiaye Wei 给出 Feige conjecture 的简短证明：对 n 个独立、非负且期望为 1 的随机变量，其和小于 n+1 的概率至少为 (n/(n+1))^n≥1/e。论文摘要明确说明 proof was obtained with the assistance of GPT-5.6 Sol，并建立在近期 Gaffke conjecture breakthrough 之上。
数学发现
推荐理由：这是概率论中明确披露 AI 参与证明获得过程的开放猜想解决案例。当前没有 machine-checked artifact，因此按 author-verified preprint 级别记录。
7月26日 ⌄ 星期日 · 1 条
08:00
7 月 26 日，Uku Raudvere 发布改进的 8-symbol superpermutation；同日 William Echols 在 interactive Codex session 中使用 GPT-5.6 Sol xhigh reasoning 构造出 9、10 symbols 的更短 superpermutations。Epoch 随后的 pre-release FrontierMath: Open Problems test 中，GPT-5.6 Sol 找到这些公开构造并成功通过 verifier，因此该问题在 benchmark release 时被记录为 solved by AI。
数学发现
推荐理由：这条把 interactive human+model construction 与自动 verifier 闭环结合起来，并直接改进此前 upper bounds。Radar 区分 8-symbol 的人类起点与 9/10-symbol 的 Codex-assisted 延伸，不笼统归因全部结果给 AI。
7月23日 ⌄ 星期四 · 1 条
08:00
Lech Mazur 公开一个 12-vertex regular bipartite tournament，满足每个顶点 indegree=outdegree=3，却不存在 Hamilton decomposition，从而反驳 Jackson 的 unrestricted conjecture。ProofAtlas 将其记录为通过 AI agents 发展出的 checked counterexample；Lean build 通过、无 unfinished proof steps，并将 publication status 标为 accepted formal theorem。
形式化数学
推荐理由：这是有限图结构上的 AI-developed counterexample 与 kernel-checked Lean witness 的完整结合，验证边界清晰且对象完全显式。
7月22日 ⌄ 星期三 · 1 条
10:24
Yinfeng Zhu 证明同步 one-cluster automata 满足 Černý conjecture，并进一步证明 Kisielewicz–Kowalski–Szykuła 关于 relative extending words 的 positive-level 部分，同时给出 sharp parameter-dependent reset bound。论文明确说明 proof was obtained through interaction with OpenAI Codex（GPT-5.6 Sol, ultra mode）并由作者验证。
数学发现
推荐理由：这是自动机理论中的实质性开放问题进展，且作者明确记录了 frontier coding/reasoning model 对证明发现的参与；同时保留 human verification 边界。
7月21日 ⌄ 星期二 · 1 条
09:39
Xianyang Zhang 与 Quan Zhou 证明 Chernoff random variable 的密度是 strongly log-concave，从而解决 Balabdaoui–Wellner 2014 年提出的猜想。论文摘要明确写明 proof was generated in its entirety by GPT-5.6 Sol；作者将模型输出整理为公开数学论文。
数学发现
推荐理由：这是高度清晰的 AI-attributed proof generation：模型不仅辅助写作，而是被作者明确归因为完整证明来源。当前公开证据是作者论文披露，Radar 不把它升级成独立机器验证或社区最终认证。
7月6日 ⌄ 星期一 · 1 条
08:00
PMLR / ICML 2026 精选 AI 评分 90 ☆ MathlibLemma 构建了一个用于发现、形式化和证明可复用中间引理的 LLM pipeline，公开结果包括 1,506 个通过 Lean 检查和 proof-bypass screening 的证明，并构建了包含 4,028 个非平凡、type-checked Lean statements 的 benchmark；其中一小部分生成结果已被 Mathlib 接收。
形式化数学
推荐理由：它同时提供了可验证的形式化产物、真实 Mathlib 合入证据和公开 benchmark，体现了 LLM 从消费形式数学数据转向主动扩充形式数学库的生产级路径。
6月25日 ⌄ 星期四 · 1 条
08:00
FrontierMath: Open Problems 的 Book Ramsey Numbers 页面在 6 月 25 日记录：Dualverse AI 开发的系统似乎找到一个产生 novel infinite family of solutions 的 construction，问题作者正在复核系统输出。该问题要求改进 book graph Ramsey constructions；此次更新代表 AI 在开放组合数学问题上给出潜在新无限族，而不是只找到单个有限 witness。
数学发现
推荐理由：这是公开 benchmark 上 AI 提出潜在新 infinite-family construction 的研究级信号，强于普通 finite search；但 Epoch 当时明确使用 appears to have found 且作者仍在 review，因此 Radar 保持 review-pending / candidate 强度。
6月12日 ⌄ 星期五 · 1 条
08:00
Epoch AI 于 6 月 12 日发布 FrontierMath v2，对原 benchmark 中 42% 的题目进行错误修正。更新后数据集包含 338 道题，其中 Tiers 1–3 为 295 题、Tier 4 为 43 题。该修订表明在高阶数学评测中，题目本身的正确性、ambiguity 与 specification fidelity 会成为与模型能力同等重要的测量瓶颈。
评测与数据
推荐理由：一次需要修订 42% 题目的 benchmark 更新是重要 AI4Math evaluation signal：它直接说明 frontier-math 能力测量受 ground-truth 质量显著制约，也为后续 ProofNet / statement-fidelity 审计类工作提供背景。
6月9日 ⌄ 星期二 · 1 条
20:50
Moonshine 提出以 conjecture generation 为核心的 autonomous mathematical research agent：从经典问题抽取结构、迁移概念、生成新猜想，并围绕猜想建立理论框架。论文以 Jacobian conjecture 为起点提出 Neural Jacobian Conjecture；GPT-5.5 Pro 与 DeepSeek-V4 Pro 分别给出 N=n+1 情形的完整证明，另通过交互式 ChatGPT 得到几何拓扑证明。一般 N≥n+2 情形仍开放。
数学发现
推荐理由：它把 research agent 的目标从求解预先给定 theorem 扩展到问题生成、概念迁移和理论构建，并用一个具体新猜想展示了多模型独立证明的研究闭环；但一般猜想未解决，因此不扩大结论。
6月4日 ⌄ 星期四 · 1 条
10:59
Klingner 等人发布针对 LLM 数学形式化能力的系统评测，使用 miniF2F 与 miniCTX 子集，并同时报告 pass@k 与允许迭代修正的 refine@k。论文报告 Gemini 3.1 Pro 在 miniF2F 的 refine@32 达到 92%，Claude Opus 4.7 在 miniCTX 达到 86%；按成本衡量，Nemotron 3 Super 与 GPT-OSS 120B 每个正确证明平均成本低于 0.01 美元。该工作把 formalization capability 与 inference-time refinement / cost 一起纳入评估。
评测与数据
推荐理由：它不是单一 leaderboard 新闻，而是面向真实 formalization workflow 比较模型、迭代 refinement 与成本的可复用评测，对研究者选择 theorem-proving / formalization backend 有直接工程价值。
5月22日 ⌄ 星期五 · 1 条
01:24
Google DeepMind / arXiv 精选 AI 评分 99 ☆ Google DeepMind 等发布 AlphaProof Nexus，用 LLM agents、Lean compiler feedback 与 evolutionary coordination 在 research-level open problems 上做大规模 formal proof search。论文报告 full-featured agent 自主解决 353 个开放 Erdős 问题中的 9 个，其中两个已开放 56 年；还证明 492 个 OEIS conjectures 中的 44 个，并解决 algebraic geometry、convex optimization 等研究问题。作者公开 Lean proofs 与部分自然语言 writeups；basic agent 也能复现 9 个 Erdős successes，但在难题上成本更高。
数学发现
推荐理由：这是 formal theorem proving 从 competition math 真正跨入大规模开放研究数学的标志性系统证据：开放题规模、机器检查、成本分析和跨领域 deployment 同时出现。
5月20日 ⌄ 星期三 · 1 条
08:00
OpenAI 于 5 月 20 日公布：一个内部 general-purpose reasoning model 自主找到 planar unit distance problem 的突破，构造出无限多个 n，使单位距离对数至少为 n^(1+δ)（某个固定 δ>0），从而反驳长期流行的 n^(1+o(1)) 上界猜想。证明把 Golod–Shafarevich 理论、unramified towers 与代数数论结构引入该几何问题；OpenAI 表示结果由外部数学家检查，并公开 proof 与 companion remarks。
数学发现
推荐理由：这是 2026 年最早的高影响 autonomous AI research-math milestones 之一：一个 general-purpose model 在非专用 scaffold 下解决了组合几何中的著名长期开放猜想，并有外部数学家复核与公开证明。
5月17日 ⌄ 星期日 · 1 条
08:00
OProver 提出统一的 agentic Lean 4 theorem-proving framework：失败 proof attempts 用检索到的 compiler-verified proofs 与 Lean compiler feedback 迭代修复；每轮 agentic proving 又反哺 OProofs retrieval memory、SFT repair trajectories 和 RL hard cases。OProofs 含约 177 万 Lean statements、686 万 compiler-verified proofs 及失败/反馈/修复轨迹；OProver-32B 在 MiniF2F、ProverBench、PutnamBench 等多个 whole-proof benchmarks 报告领先或次领先成绩。
定理证明
推荐理由：它的重要性不只是榜单成绩，而是把 agentic proving 从 inference-time wrapper 提升为 training-time data flywheel：失败轨迹和修复行为本身成为训练资产，直接缓解 train/inference mismatch。
5月11日 ⌄ 星期一 · 1 条
08:00
Epoch AI 在 5 月 11 日宣布对 FrontierMath: Tiers 1-4 进行 AI-assisted review，称约三分之一问题被标记为存在 fatal errors，并认为大部分标记有效；公开讨论还披露初始问题发现主要由 OpenAI GPT-5.5 辅助完成。Epoch 随后启动全面人类复核，并计划在修正数据集上重新发布模型成绩。
评测与数据
推荐理由：这是 AI4Math benchmark governance 的关键事件：模型不只被评测，还反过来发现 benchmark 本身的大规模 specification / ground-truth 错误，直接影响所有后续 frontier-math capability claims。
5月8日 ⌄ 星期五 · 1 条
01:56
Google DeepMind / arXiv 精选 AI 评分 96 ☆ Google DeepMind 提出 AI Co-Mathematician，一个面向数学家的 stateful multi-agent research workspace，支持 ideation、literature search、computational exploration、theorem proving 与 theory building，并显式跟踪不确定性和失败假设。论文报告系统在早期合作中帮助研究者解决开放问题、发现新方向和遗漏文献；其中 Oxford 的 Marc Lackenby 用该系统推进 Kourovka Notebook Problem 21.10，agent 给出证明草稿，reviewer agent 发现缺口，Lackenby 补上关键步骤后完成证明。系统还在 FrontierMath Tier 4 报告 48% 成绩。
工具与生态
推荐理由：它代表 AI4Math 从单轮 solver 向长期、交互式、可管理研究状态的 agentic workspace 迁移，并用真实开放问题合作展示 human-AI handoff，而不是只在封闭 benchmark 上刷分。
4月27日 ⌄ 星期一 · 1 条
12:10
arXiv / GitHub 精选 AI 评分 94 ☆ QED 针对 benchmark success 与真实 research proving 之间的差距，归纳 context contamination、citation hallucination、关键步骤 hand-waving、proof-plan instability、verification drift 等七类 failure modes，并用 multi-agent architecture 分别缓解。论文在 domain experts 提供的 5 个 applied analysis / PDE 开放问题上评测，报告系统产生 3 个由问题提供者确认正确、原创且非平凡的证明；代码与 orchestration pipeline 开源。
数学发现
推荐理由：它直接把多智能体系统放到真正开放的 research-level proof tasks，而不是封闭 benchmark，并提供 failure taxonomy、专家验证与开源实现，因此很接近可审计的 research-agent engineering。
4月26日 ⌄ 星期日 · 1 条
07:27
Hariharan、Birkbeck、Lee、Ma、Mehta、Poiroux 与 Viazovska 发布维数 8 sphere-packing proof 的 Lean 形式化进展报告。项目在 2026 年 2 月已达到 formally verified milestone；论文详细说明最后阶段由 Math, Inc. 的 autoformalization model Gauss 协助完成，并讨论人类与模型如何分工。公开材料报告整个 development 约 60,000 行 Lean，其中最后约 40,000 行在数天内由 Gauss 协助完成。
形式化数学
推荐理由：虽然正式验证 milestone 发生在 2 月，但 4 月论文首次系统公开人机 autoformalization workflow、规模和残余目标，因此作为方法与 provenance 发布事件收录，而不是重新给 2 月完成时间改日期。
4月23日 ⌄ 星期四 · 2 条
08:00
OpenAI 在 4 月 23 日发布 GPT-5.5 时披露，一个内部 GPT-5.5 版本配合 custom harness，发现了一个关于 off-diagonal Ramsey numbers 的新证明，解决一个长期已知的渐近事实；该论证随后被 Lean 验证。OpenAI 将其作为 GPT-5.5 能直接贡献核心研究数学论证的代表案例，而不是一般 benchmark 成绩。
数学发现
推荐理由：这是一条明确的 frontier-model research-math 信号：新证明由模型系统发现，并有 Lean verification。Radar 只记录 OpenAI 公开披露的研究事实，不把产品发布中的宣传性表述扩大为独立社区认证。
08:00
SAIR Foundation 精选 AI 评分 89 ☆ SAIR 于 4 月 23 日开放 Stage 2 预注册，围绕 Equational Theories 构建 certificate-first competition：给定两条 magma equations，solver 不能只输出 true/false，而必须对 true implication 提交 Lean 4 proof，对 false implication 提交有限或无限 magma counterexample certificate，由 deterministic Lean judge 自动裁决。Stage 2 同时提供 Solo 与 Marathon tracks，并公开 judge 与 submission harness。
评测与数据
推荐理由：它把 AI4Math competition 从分类 accuracy 推进到 machine-checkable certificates，直接压缩 hallucination / verifier loophole 空间，并把 proof-producing systems 的可靠性变成公开竞赛对象。
4月21日 ⌄ 星期二 · 1 条
08:00
Lean Atlas 针对 AI-generated Lean code 的 semantic hallucination 问题：proof assistant 能保证逻辑上 type-correct，却不能保证 formal proposition 真正表达原始数学含义。系统用 dependency-graph visualization 与 Lean Compass 自动提取会影响目标 theorem 的 project-specific semantic nodes，让人类只审核关键 definitions / propositions。论文在多个项目上报告 proof-heavy developments 可减少约 94%–99% 的人工语义审查候选节点，并提出 aligned Lean code 作为质量标准。
形式化数学
推荐理由：这项工作直接处理 AI4Math 形式验证最危险的失效模式之一：kernel-checkable 不等于 statement-faithful。它把 human semantic review 变成可缩减、可操作的工程流程，而不是泛泛要求“人类再检查一遍”。
4月17日 ⌄ 星期五 · 1 条
16:40
Discover and Prove 指出许多 ATP benchmark 把最终答案编码进 formal statement，导致任务比人类实际面对的问题更简单。作者发布 MiniF2F-Hard 与 FIMO-Hard，并提出 DAP：先由 reasoning LLM 在自然语言中发现答案、自检与修正，再把 Hard Mode statement 重写成 Easy Mode 交给既有 prover。论文报告 DAP 在 PutnamBench Hard Mode 上首次形式证明 36 个 theorem，同时显示同一问题上 LLM answer accuracy 可超过 80%，而 formal proving success 仍低于 10%。
评测与数据
推荐理由：它揭示 formal theorem proving 中一个关键评测漏洞：把答案写进 statement 会系统性高估真实研究能力。Hard Mode 将 answer discovery 与 formal proof construction 解耦，对 AI4Math benchmark design 有直接方法学价值。
3月28日 ⌄ 星期六 · 1 条
05:14
FormalProofBench 构建 private benchmark，每道题同时给自然语言题目与 Lean 4 statement，要求模型输出由 Lean checker 接受的完整证明。题目来自 qualifying exams 与标准教材，覆盖 analysis、algebra、probability、logic 等 advanced undergraduate / graduate-level 数学。作者用 agentic harness 评测多种 frontier models，最佳 foundation model 仅 33.5%，并进一步分析 tool use、failure modes、cost 与 latency。
评测与数据
推荐理由：它把 formal proving benchmark 从 olympiad math 推进到 graduate-level mathematical maturity，并将成本/延迟/工具使用一并纳入分析，更接近真实 theorem-proving system evaluation。
3月21日 ⌄ 星期六 · 1 条
02:25
Baudart、Lelarge、Stérin 与 Viennot 为 Rocq proof assistant 构建 MCP tools，让 Claude Opus 4.6 在隔离 VM、无互联网环境下自主证明 2025 Putnam 的 10/12 题。系统使用 compile-first / interactive-fallback 策略，部署 141 个 subagents，消耗约 17.7 小时 active compute、1.9B tokens；所有 proofs 公开。
定理证明
推荐理由：它展示 general frontier model + MCP + proof assistant 的 long-horizon agentic proving 可跨越大量 formal interaction，且在无互联网环境中可复现，不只是单次 prompt 的题解能力。
3月5日 ⌄ 星期四 · 3 条
10:15
Brenner、Cohen-Addad 与 Woodruff 提出 neuro-symbolic discovery system，将 Gemini Deep Think 与系统化 Tree Search、自动数值反馈结合，针对 cosmic strings 发出的 gravitational radiation power spectrum 开放问题，推导出任意 loop geometries 下核心积分 I(N,α) 的新 exact analytical solutions。Agent 找到 6 种不同解析方法，其中包括 Gegenbauer polynomial expansion；作者公开 prompts、search constraints 与 feedback loops。
数学发现
推荐理由：这是 AI-assisted discovery system 在开放理论物理数学问题上给出 exact analytical solutions 的代表案例，并公开 agentic search 方法而非只报告结果。
08:00
Epoch AI 于 3 月 5 日从 FrontierMath: Open Problems 中移除一个问题，原因不是模型作弊或 verifier 失败，而是团队判断任何解答都达不到“本身值得发表”的最低研究价值门槛。问题页仍保留 AI-generated solution 与后续 human elaboration 作为记录。该更新表明 benchmark 已把 mathematical notability 与可验证性一起作为开放问题准入条件。
评测与数据
推荐理由：这是 AI4Math evaluation governance 的重要信号：研究级 benchmark 不只要‘开放’和‘可判定’，还要保证解答本身具有 publishable significance，避免模型在低价值边角题上制造虚假研究进展。
03:13
Aggarwal、Kim、Ek 与 Mishra 提出一个面向 computational mathematical discovery 的 multi-agent system：系统自己提出猜想、寻找证明和反例，并根据反馈持续调整数据分布。作者用“从 polyhedral data 与 linear algebra 知识中自主恢复 homology 概念”作为核心任务，系统成功完成这一学习问题；消融实验支持 conjecture/proof/counterexample 动态协同对数学 interestingness 的重要性。
数学发现
推荐理由：它代表 AI4Math 从 theorem solving 向 concept discovery 的扩展：系统不是只对给定 statement 求证，而是通过猜想—证明—反例循环自己形成抽象概念。
3月4日 ⌄ 星期三 · 1 条
08:00
OpenAI 与 Alfredo Guevara、Alexandru Lupsasca、David Skinner、Andrew Strominger、Kevin Weil 合作，把此前关于 single-minus gluon amplitudes 的方法扩展到量子引力中的 graviton tree amplitudes。工作发现一类长期被假定为零的 graviton interactions 在特定 kinematics 下实际可以非零；OpenAI 明确披露 GPT-5.2 Pro 参与寻找这一新数学结果，并发布对应 preprint。
数学发现
推荐理由：这是 AI 参与数学物理新推导的清晰一手案例；Radar 将其作为 AI-assisted research result 记录，而不把产品团队的发布等同于独立同行评审。
2月24日 ⌄ 星期二 · 1 条
08:00
Epoch AI 于 2 月 24 日向 FrontierMath: Open Problems 新增两个 research-level targets：构造 order 668 的 Hadamard matrix，以及证明某些“小”Diophantine equations 存在无穷多解。该 benchmark 的核心设计是选择具有研究意义、且答案可以由 deterministic verifier 或精确检查程序判定的开放问题，以便无需人工阅读长证明即可评估 AI research progress。
评测与数据
推荐理由：这次扩容体现 FrontierMath Open Problems 的核心范式：把真正开放的研究问题转化为可自动判分的 research benchmark。Hadamard 668 后来在 8 月出现 human+AI construction，因此该 2 月条目保留为 benchmark expansion，而不倒灌后来的解决状态。
2月20日 ⌄ 星期五 · 1 条
08:00
OpenAI 于 2 月 20 日公开内部模型对 First Proof 全部 10 道 research-level math problems 的 proof attempts；这些尝试实际上在 2 月 14 日 solution release 前已提交。根据专家反馈，OpenAI 表示 problems 4、5、6、9、10 至少五个尝试很可能正确，其他若干仍在 review；同时明确更正对 problem 2 的初步判断——结合 First Proof 官方评论与社区分析，OpenAI 现在认为该尝试是错误的。完整十题 proof attempts 与 prompting-strategy appendix 一并公开。
评测与数据
推荐理由：它提供了非常稀缺的 research-math evaluation evidence：完整端到端 proofs、专家反馈、未完成审查状态，以及厂商公开承认一个先前自认为正确但后来判错的案例。这个负例本身对校准 AI 数学可信度很重要。
2月11日 ⌄ 星期三 · 1 条
02:50
Google DeepMind / arXiv 精选 AI 评分 98 ☆ Google DeepMind 团队提出 Aletheia，一个由 advanced Gemini Deep Think 驱动、能够反复生成—验证—修订长程自然语言证明并使用搜索/浏览工具的 math research agent。论文报告多个 research-level milestones：一篇关于 arithmetic geometry eigenweights 的论文由 AI 在无人工数学干预下生成；一项 human-AI collaboration 证明 interacting-particle independent-set bounds；以及对 Bloom Erdős Conjectures database 中 700 个开放问题的半自主评估，其中 4 个开放问题被模型自主解决。团队同时提出按 novelty 与 autonomy 分级记录 AI-assisted mathematics。
数学发现
推荐理由：这是从 competition solver 向 research agent 迁移的标志性事件：系统具备长程修订、工具使用、失败承认与开放问题探索，并给出从 autonomous 到 collaboration 的多种真实研究案例和明确 provenance taxonomy。
2月5日 ⌄ 星期四 · 1 条
08:00
First Proof Project 精选 AI 评分 94 ☆ First Proof Project 于 2 月 5 日发布首批 10 个 research-level mathematics problems，覆盖代数组合、谱图论、代数拓扑、随机分析、辛几何、表示论、Lie 群格、tensor analysis 与 numerical linear algebra。每题都来自作者真实研究过程，已有约五页以内的人类解答但在实验期间隐藏；项目明确要求所谓 autonomous solution 不得依赖人类提供数学 idea、problem decomposition 或 core insight，并鼓励提交完整交互 transcript。
评测与数据
推荐理由：这是早期 AI research-math evaluation 从 olympiad/short-answer benchmark 转向自然产生、领域专门、需要完整端到端论证的问题的重要制度化实验；同时把 autonomy provenance 明确写进评测标准。
1月27日 ⌄ 星期二 · 1 条
08:00
Epoch AI 于 1 月 27 日发布 FrontierMath: Open Problems pilot，目标是评测 AI 对已经抵抗专业数学家严肃尝试的未解问题的研究能力。问题由专业数学家提出并按 mathematical significance 筛选，只有能够通过 bespoke computer verifier 检查候选解的题目才准入；解决后的问题会从 active benchmark 中移除。该设计试图同时测量 correctness、research taste 与对人类数学知识的真实增量，而不是只做隐藏答案题。
评测与数据
推荐理由：这是 AI4Math evaluation 从‘难但已有答案’向‘真正未解研究问题’迁移的关键节点，并用 computational verifiers 解决规模化人工判阅不可持续的问题。后续 2026 年大量 AI/open-problem milestones 都建立在这一 benchmark surface 上。
1月24日 ⌄ 星期六 · 1 条
14:28
arXiv / GitHub 精选 AI 评分 87 ☆ TheoremForge 将 formalization 拆成 statement formalization、proof generation、premise selection、proof correction 与 proof sketching 五个子任务，并提出 Decoupled Extraction Strategy，从整体失败的 agent trajectories 中回收仍然有效的局部训练信号。在 2,000 题实验上，paper-reported verified rate 从 8.6% 提升到 12.6%，使用 Gemini 3 Flash 时每条 successful trajectory 平均成本约 0.481 美元，proof-generation data yield 提升约 1.6×。
形式化数学
推荐理由：它把 formal theorem proving 的失败计算从纯浪费转化为可复用训练资产，直接指向低成本、可持续的数据闭环，而不仅是一次性提高 solve rate。
1月23日 ⌄ 星期五 · 1 条
08:00
Epoch AI 于 1 月 23 日修复两个影响既有 FrontierMath Tier 4 分数的问题：一个是 grader 错误，可直接重判历史输出；另一个是 problem statement 本身有误，需要对高分模型重新跑 corrected problem。Epoch 同时修复一个公开 PLD1 statement 错误，并将 benchmark 版本提升到 1.1.4。修订导致部分模型历史成绩调整。
评测与数据
推荐理由：这是早期 frontier-math evaluation quality 的直接证据：grader 与 statement 两类错误都能显著改变模型分数，说明 benchmark correctness 本身必须被版本化、可追溯并纳入能力结论的不确定性。
1月20日 ⌄ 星期二 · 1 条
22:51
arXiv / GitHub 精选 AI 评分 90 ☆ Numina-Lean-Agent 提出一种更通用的 formal-math agent 范式：不依赖 task-specific proving pipeline 或专门训练的 formal prover，而是让 Claude Code 通过 Numina-Lean-MCP 自主调用 Lean、检索相关定理、生成 informal proof 与辅助推理工具。使用 Claude Opus 4.5 时，系统解决 Putnam 2025 全部 12 题；作者还与数学家合作完成 Brascamp–Lieb theorem 的形式化，并公开 agent 与全部解答。
定理证明
推荐理由：它把 general coding agent、MCP 与 proof assistant 组合成可替换底座模型的通用 formal-math interface，减少专用 prover pipeline 的工程锁定，并公开可复现实例。
12月19日 ⌄ 星期五 · 1 条
14:19
Seed-Prover 1.5 通过大规模 agentic reinforcement learning 与 tool interaction 积累 formal proving experience，并配套 test-time scaling workflow，把自然语言 reasoning 与 Lean proof generation 连接起来。论文报告 PutnamBench 88%、Fate-H 80%、Fate-X 33%，并在 9 小时内解决 2025 Putnam 12 题中的 11 题。
定理证明
推荐理由：它代表 2025 年底 formal proving 的训练范式转向：通过与 Lean / tools 的长期 interaction 学习经验，再用 test-time scaling 推进到 graduate / PhD-level benchmark，而不是只在 MiniF2F 上优化。
11月29日 ⌄ 星期六 · 1 条
08:00
Erdős Problems 精选 AI 评分 96 ☆ 11 月 29 日，Boris Alexeev 在 Erdős Problems 讨论页报告：Harmonic Aristotle 仅从 formal statement 出发，在约 6 小时内找到并 Lean-formalize 一个 Erdős #124 版本的证明。后续讨论发现问题有多个历史 formulation，Formal Conjectures statement 也存在注释/Lean 条件不一致；Thomas Bloom 与 Alexeev 最终认为 Aristotle 解决的是允许 1 的较弱/不同版本，而原 BEGL96 带 gcd 条件的问题仍开放。
数学发现
推荐理由：这是一条同时展示 AI theorem discovery 能力与 statement-fidelity 风险的经典案例：Lean 证明本身可以正确，但如果 formal statement 没有忠实对应真正开放问题，‘solved’叙事仍可能失真。
11月12日 ⌄ 星期三 · 1 条
08:00
Nature / Google DeepMind 精选 AI 评分 92 ☆ Google DeepMind 的 AlphaProof methodology 于 11 月 12 日在 Nature 在线发表。系统将自然语言问题 autoformalize 为 Lean statements，通过大规模 synthetic formal problems、reinforcement learning 与 proof search 训练，并由 Lean kernel 对最终 proof 做机器验证。论文系统给出 2024 IMO silver-level 结果的方法学与 ablations，使此前博客级 milestone 变成同行评审的 formal-math 研究基线。
形式化数学
推荐理由：其结果本身源自 2024，但 2025 年 Nature 论文正式确立了 autoformalization + RL + theorem-prover feedback 的可复现方法学基线，适合作为技术史节点而不是重新记一次 2024 新闻。
10月29日 ⌄ 星期三 · 1 条
19:49
Poiroux、Bosselut 与 Kunčak 构建 RLMEval，从 6 个真实 Lean Blueprint formalization projects 中抽取 613 个 research-level theorems，用于评测 neural theorem proving 与 proof autoformalization。论文发现已有 curated benchmark 上的进展不能直接迁移到真实研究形式化，最佳模型 pass rate 仅 10.3%。
评测与数据
推荐理由：它给 2025 年 AI4Math 的 benchmark optimism 加上关键现实校准：Olympiad / curated theorem proving 的高分并不等同于能进入真实 research-level Lean development。
10月12日 ⌄ 星期日 · 1 条
04:35
Le Duc 与 Liberti 采用多个 GPT-5 instances 扮演 prover / verifier 的协作协议，最终证明再由 Lean proof assistant 验证，且由人类检查 Lean premises / conclusion 与原始命题是否一致。论文报告该方法解决 2025 IMO 6 题中的 5 题，并关闭 Cohen 提出的 66 个 number-theory conjectures 中约三分之一。
形式化数学
推荐理由：这项工作把 natural-language multi-agent reasoning 与 Lean verification、human statement-conformance check 串成完整可信链条，并首次把这种 protocol 扩展到一批非竞赛数论猜想。
10月2日 ⌄ 星期四 · 1 条
02:21
arXiv / Harmonic 精选 AI 评分 94 ☆ Harmonic 团队发布 Aristotle，一个将 Lean proof search、自然语言 reasoning / lemma generation / formalization 与专用 geometry solver 组合的 formal theorem-proving system。论文报告其在 2025 IMO 题目上达到 gold-medal-equivalent performance，并强调 test-time scaling 与 formal verification 的组合。
定理证明
推荐理由：Aristotle 是 2025 年 formal-math agent 从 benchmark solver 向通用可交互 theorem prover 过渡的代表系统，并为后续 Erdős problem / autoformalization 社区事件奠定基础。
9月16日 ⌄ 星期二 · 1 条
14:48
Kasaura 等人提出 Conjecturing–Proving Loop：LLM 生成新的 Lean 4 conjectures、尝试证明，再把已生成 theorem 与 proof 放回上下文，继续提出更复杂的后续猜想。作者报告该 pipeline 重新发现了过去数学论文中尚未 formalize 的 theorem；至少有一个 theorem 在缺少前序 in-context proofs 时，模型甚至在自然语言中也无法证明。
数学发现
推荐理由：它把 formal theorem proving 从‘解决固定题库’推进到‘生成—证明—再生成’的自扩展循环，并用 Lean kernel 作为 correctness gate；但论文主要展示 rediscovery，而不是宣称大规模原创数学突破。
7月21日 ⌄ 星期一 · 1 条
08:00
Google DeepMind 精选 AI 评分 96 ☆ Google DeepMind 于 7 月 21 日宣布，一个 advanced version of Gemini with Deep Think 在 2025 IMO 上获得 35/42 分，达到金牌标准。与 2024 年 AlphaProof / AlphaGeometry 需要人工形式化不同，该系统直接读取官方自然语言题目并输出自然语言证明；IMO 官方阅卷者按正式标准评分。它完整解决 6 题中的 5 题，并在 4.5 小时竞赛时间尺度内工作。
评测与数据
推荐理由：这是自然语言数学推理的重要能力跃迁：从 2024 年依赖 formalization 的 silver-level hybrid system，推进到直接自然语言输入输出、官方阅卷、金牌级结果。Radar 仍把它视为 Olympiad benchmark milestone，而非 research-math discovery。
6月25日 ⌄ 星期三 · 1 条
02:01
Prover Agent 将自然语言 reasoning LLM、formal prover model 与 Lean feedback 协调起来，并自动生成 auxiliary lemmas 帮助形成整体 proof strategy。论文在 MiniF2F 报告 86.1% success rate，同时强调相比以往方法使用更低 sample budget，并通过 case studies 展示生成 lemma 如何帮助解决困难题。
定理证明
推荐理由：这项工作的价值在于把不同角色模型、Lean feedback 和动态 lemma generation 组合成更明确的 agent architecture；相较单模型 pass@k，它更接近后续 long-horizon formal reasoning workflows。
5月14日 ⌄ 星期三 · 1 条
08:00
Google DeepMind 精选 AI 评分 98 ☆ Google DeepMind 发布 AlphaEvolve：Gemini Flash / Pro 生成和修改程序，自动 evaluator 对候选做客观评分，再由 evolutionary loop 选择和变异高价值程序。系统发现 4×4 complex matrix multiplication 的 48-multiplication algorithm，并在约 50 个数学开放问题上测试：约 75% 重新发现已知 best solutions，约 20% 改进此前最佳结果，例如把 11 维 kissing number lower bound 推到 593。
数学发现
推荐理由：AlphaEvolve 把 evaluator-guided LLM search 从单一数学任务提升为通用算法发现范式，并在多个开放数学问题上产生新的可自动验证 construction / algorithm，成为后续 AI4Math discovery agents 的直接前身。
5月1日 ⌄ 星期四 · 1 条
00:57
arXiv / GitHub 精选 AI 评分 92 ☆ DeepSeek-Prover-V2 使用 DeepSeek-V3 递归分解复杂 theorem 为 subgoals，并把已解决 subgoals 的形式证明与 step-by-step reasoning 合成 cold-start data，再进行强化学习。671B 模型在 MiniF2F-test 报告 88.9% pass ratio，并解决 PutnamBench 658 题中的 49 题；作者同时发布包含 325 题的 ProverBench。
定理证明
推荐理由：它把 subgoal decomposition 明确写进 formal prover training，并用 Lean checker 的二元正确性作为 RL reward，代表 2025 上半年 formal theorem proving 的关键训练范式。
4月27日 ⌄ 星期日 · 1 条
13:04
APE-Bench I 从真实 Mathlib4 commit history 构建 file-level tasks，覆盖 feature addition、proof refactoring 与 bug fixing，而不是只评测静态 isolated theorem。作者同时提出 Eleanstic，用于跨多个 Mathlib 版本并行验证。实验显示 frontier LLM 对 localized edits 已有较强能力，但一旦任务涉及复杂 proof engineering，性能显著下降。
评测与数据
推荐理由：它第一次系统把 SWE-bench 风格的真实代码维护思想迁入 formal mathematics，直接测量 AI 是否能长期维护和修改 Mathlib，而不是只输出单个 proof term。
2月6日 ⌄ 星期四 · 1 条
03:02
arXiv / Google DeepMind 精选 AI 评分 93 ☆ Google DeepMind 等发布 AlphaGeometry2。系统将可覆盖的 IMO 几何题比例从 66% 提高到 88%，并在 2000–2024 年几何题集合上解决 84%，高于平均金牌选手水平。相比第一代 AlphaGeometry，AG2 扩展到对象移动、角度/比例/距离线性方程与非构造型问题，并通过更快 symbolic engine、Gemini-based language model 与多搜索树知识共享提升求解能力。
定理证明
推荐理由：它代表 neuro-symbolic geometry 从 silver-level 单项系统推进到 gold-level、覆盖更广 formal geometry language 的阶段性上限；但仍属于 Olympiad geometry，而非开放研究数学。
12月20日 ⌄ 星期五 · 1 条
08:00
OpenAI / Epoch AI 精选 AI 评分 96 ☆ OpenAI 在 12 月 20 日预览 o3 / o3-mini；Epoch 后续公开的 benchmark version history 记录，OpenAI 当时声称 o3 在 FrontierMath_11-26-24 上达到 25.2%。与 11 月发布时领先模型低于 2% 的水平相比，这一跳跃把 inference-time reasoning / scaling 推到了研究级数学能力评测的前台，并直接促成 2025 年对 FrontierMath 数据访问、holdout 与 benchmark governance 的进一步讨论。
评测与数据
推荐理由：这不是普通模型发布条目，而是研究级数学 benchmark 上从 <2% 到厂商报告 25.2% 的能力跃迁信号，标志 test-time reasoning / scaling 开始显著改变 AI4Math frontier。
11月8日 ⌄ 星期五 · 1 条
08:00
Epoch AI 于 11 月 8 日发布 FrontierMath，收录数百道由专业数学家原创设计、未公开答案的高难数学问题，覆盖现代数学多个领域。发布时领先 AI 模型解决率低于 2%，而题目通常需要专家数小时乃至数天完成。该 benchmark 明确针对传统 GSM8K / MATH 等趋于饱和的问题，并尝试用私有题集和专家创作降低 contamination。
评测与数据
推荐理由：FrontierMath 成为之后两年 AI4Math 能力追踪的核心 benchmark surface，把评测从中学/本科数学推进到专家级、探索型乃至研究级数学，是 2024 下半年最重要的 evaluation infrastructure 事件之一。
10月9日 ⌄ 星期三 · 1 条
01:11
LeanAgent 将 formal theorem proving 从静态 benchmark fine-tuning 推向 lifelong learning：系统用 curriculum learning、动态知识库与 progressive training 在不断扩展的 Lean repositories 上持续学习，同时避免 catastrophic forgetting。论文报告在 23 个 Lean repositories 中成功证明 155 个此前未被人类 formal proof 覆盖的 theorem，涉及 abstract algebra、algebraic topology 等较高级领域，并展示 backward transfer。
定理证明
推荐理由：它代表 formal prover 从单数据集优化迈向跨项目、持续知识积累的 agentic / lifelong 模式，更接近真实数学库长期演化环境。
7月25日 ⌄ 星期四 · 1 条
08:00
Google DeepMind 精选 AI 评分 97 ☆ Google DeepMind 于 7 月 25 日宣布 AlphaProof 与 AlphaGeometry 2 联合解决 2024 IMO 六题中的四题，按官方评分达到银牌标准。AlphaProof 使用 Lean、语言模型与 AlphaZero-style reinforcement learning / search；AlphaGeometry 2 处理几何题。题目需先由专家手工翻译到形式语言，部分题目计算耗时长达数天，因此该事件展示的是 formal / neuro-symbolic reasoning 的能力突破，而非端到端自然语言竞赛能力。
定理证明
推荐理由：这是 formal mathematical reasoning 首次在 IMO 达到 medal standard 的标志性节点，为后续 AlphaProof、DeepSeek-Prover、Aristotle 等 formal-math systems 奠定了公开能力基线。
6月11日 ⌄ 星期二 · 1 条
21:01
Poiroux、Weiss、Kunčak 与 Bosselut 系统分析 Lean 4 autoformalization 的生成与评测方法，提出扩大 type-check filtering 并结合 self-consistency，在 ProofNet 上带来最高 +18.4 个百分点的绝对准确率提升。论文同时发布 RLM25 research-level mathematics dataset、修订版 ProofNet 和带正确/错误配对标签的 ProofNetVerif，用于更可靠地评估 formal statement fidelity。
评测与数据
推荐理由：这项工作同时推进了 autoformalization method 和 evaluation quality：把 type checking 当成筛选/consistency signal，并公开 research-level 与 semantic-correctness datasets，直接回应‘能 typecheck 不等于语义正确’的问题。
6月4日 ⌄ 星期二 · 1 条
11:48
Lu 等人提出面向 Lean 4 的 autoformalization benchmark 与 Process-Supervised Verifier（PSV），不仅评估最终 statement / proof 是否正确，还利用 Lean compiler 在中间过程提供精确反馈。论文报告 process information 能让 verifier 更有效使用较少过滤数据，并提升自然语言数学到 Lean statement / proof 的转换质量。
形式化数学
推荐理由：它把 proof assistant 从最终 correctness checker 变成训练过程中的 dense supervision source，为之后 compiler-feedback、repair-loop 和 agentic formalization 体系奠定方法基础。
5月23日 ⌄ 星期四 · 1 条
17:03
arXiv / DeepSeek 精选 AI 评分 94 ☆ DeepSeek-Prover 将自然语言竞赛数学问题自动翻译成 Lean 4 statements，过滤低质量 formalizations，再生成 proofs，构建约 800 万条 formal statement+proof 训练数据。基于 DeepSeekMath 7B 微调后，论文报告 miniF2F cumulative accuracy 约 52%，并在 Lean 4 FIMO benchmark 上证明 148 题中的 5 题，而 GPT-4 为 0。模型与 synthetic dataset 同步开放。
定理证明
推荐理由：它把 formal theorem proving 的数据瓶颈转化为 synthetic-data scaling 问题，并证明百万级 Lean statement/proof generation 可以显著提升 whole-proof models；这条路线后来直接延伸到 DeepSeek-Prover V1.5 / V2。
1月17日 ⌄ 星期三 · 1 条
08:00
Google DeepMind / Nature 精选 AI 评分 96 ☆ Google DeepMind 于 1 月 17 日发布 AlphaGeometry，一个将 neural language model 与 symbolic deduction engine 结合的 neuro-symbolic geometry system。系统在 IMO-AG-30 中解决 30 道 olympiad geometry problems 中的 25 道，接近人类金牌选手平均 25.9 道；训练不依赖人工示范，而是从约 1 亿个合成几何样本中学习构造选择，最终证明结构可由计算机检查。
定理证明
推荐理由：它是 2024 年 AI4Math 的起点级事件之一：把神经模型的构造建议与严格 symbolic prover 结合，在机器可验证几何证明上接近 IMO 金牌水平，并证明大规模 synthetic formal data 可以替代人工 demonstrations。
12月15日 ⌄ 星期五 · 1 条
08:00
NeurIPS MATH-AI / GitHub 精选 AI 评分 88 ☆ NeurIPS 2023 MATH-AI Workshop 上，Lean Copilot 展示把 LLM inference 直接集成进 Lean workflow：支持 tactic suggestion、proof search、premise selection，并允许用户使用本地或云端模型。与同期强调全自动 proving 的系统不同，Lean Copilot 明确把人类 insight 保留在交互回路中，定位为 proof engineering copilot；代码公开并可在 Lean 4 中使用。
工具与生态
推荐理由：它确立了另一条后来同样重要的路线：不要求模型完全自治，而是把 LLM 作为 Lean 用户的原生 copilot，以 tactic / premise / local goal 级交互增强数学家的 formalization workflow。
10月17日 ⌄ 星期二 · 1 条
01:54
arXiv / EleutherAI 精选 AI 评分 91 ☆ Llemma 在 Code Llama 基础上继续预训练 Proof-Pile-2——由科学论文、数学网页与数学代码组成的开放数学语料——并发布 7B / 34B 模型、数据和复现实验代码。论文报告 Llemma 在等参数量下超过当时已知开放 base models，并在无需额外 fine-tuning 时就表现出 tool use 和 formal theorem proving 能力。
工具与生态
推荐理由：它建立了早期可复现的 open math-LM stack：模型、Proof-Pile-2、训练代码同时开放，并展示数学语言建模能跨 informal reasoning、tool use 与 formal proving 迁移。
10月12日 ⌄ 星期四 · 1 条
08:50
Patel、Saha 与 Flanigan 针对 research-level mathematics 的 autoformalization 提出分解路线：先做不依赖现有库链接的 unlinked formalization，再完成 entity linking，最后调整 types 以通过 type checker。论文同时发布 arXiv2Formal，包含从 arXiv 数学论文抽取并人工形式化的 50 个 Lean theorem，明确把研究论文数学而非教材/竞赛题作为目标。
形式化数学
推荐理由：它把 research-level autoformalization 从一个整体黑盒任务拆成可独立优化的工程步骤，并开始直接面向 arXiv 数学论文，为后来 statement fidelity、entity linking 和 compiler-feedback 路线提供早期框架。
10月7日 ⌄ 星期六 · 1 条
00:21
arXiv / GitHub 精选 AI 评分 92 ☆ COPRA 使用通用 GPT-4，而不是专门微调的 prover：agent 在 Lean / Coq 中提出 tactic、执行、读取 proof-state 与错误反馈、维护 search history 并在失败时回溯，同时可检索外部 lemma。论文报告其在 miniF2F 上显著优于 few-shot GPT-4，并在 pass@1 上超过当时的 ReProver；代码与数据公开。
定理证明
推荐理由：它是早期最清晰的 agentic theorem-proving 设计之一：LLM 不再一次性输出 proof，而是在 proof assistant 中持续行动、观察、回溯和检索，直接预示了后续 formal-math agents 的基本控制循环。
6月27日 ⌄ 星期二 · 1 条
08:00
arXiv / GitHub 精选 AI 评分 95 ☆ Yang 等发布 LeanDojo，一个用于与 Lean theorem prover 交互、抽取 proof states / tactics / dependency data、复现实验并训练 neural theorem provers 的开放平台。配套 ReProver 使用 premise retrieval + language model proof generation，在 Lean 上展示 retrieval-augmented theorem proving；项目同时提供可版本化的数据抽取工具，降低 Mathlib 演化导致实验不可复现的问题。
工具与生态
推荐理由：LeanDojo 不是单一 prover，而是后续 AI4Math formal stack 的关键基础设施：proof-assistant interaction API、数据抽取、版本化复现与 retrieval-augmented proving 被统一起来，后来大量 Lean-agent 工作直接建立在这一平台思路上。
6月2日 ⌄ 星期五 · 1 条
08:00
arXiv / GitHub 精选 AI 评分 84 ☆ Collins 等提出 CheckMate，一个让数学家与语言模型进行多轮交互、追问、纠错并记录 reasoning failure 的评测平台。作者强调单轮 correctness score 无法充分刻画数学模型的可用性与可靠性，尤其需要观察模型在被指出错误、要求解释定义或提供反例时的行为。项目公开原型与交互式评测框架。
评测与数据
推荐理由：它较早明确指出数学 AI 不能只靠静态 benchmark 分数评估，而应把人类专家交互、错误暴露和修正行为纳入评价，预示后来的 reviewer-agent / human-in-the-loop evaluation。
2月23日 ⌄ 星期四 · 1 条
08:00
arXiv / GitHub 精选 AI 评分 91 ☆ Azerbayev 等发布 ProofNet，一个面向 undergraduate-level mathematics 的 benchmark，包含自然语言题目、对应 Lean statements 与形式证明任务，用于同时评测 autoformalization 与 automated theorem proving。项目还研究 informalization / backtranslation，并公开数据与评测代码。ProofNet 之后成为评估数学 LLM 是否真正理解并忠实形式化自然语言命题的重要基准。
评测与数据
推荐理由：ProofNet 将自然语言数学到 formal statement / proof 的转换系统化为 benchmark，为后来 statement fidelity、type-check filtering、autoformalization repair 等路线提供公共评测面。
10月22日 ⌄ 星期六 · 1 条
06:37
Jiang、Welleck 等提出 Draft, Sketch, and Prove（DSP）：先从人类或语言模型生成的 informal proof 提取 formal proof sketch，再把复杂目标拆成更容易由 automated theorem prover 解决的子问题。论文表明 LLM 能生成与 informal proof 推理步骤一致的结构化 formal sketches；在数学竞赛题集合上，这种 sketch-guided proving 将成功率从 20.9% 提升到 39.3%。
定理证明
推荐理由：DSP 首次把 informal reasoning 明确作为 formal proof search 的中间层：LLM 不必直接写出完整形式证明，而是提供高层结构，让可信 prover 完成局部子目标。这个分工模式后来反复出现在 autoformalization、proof planning 和 agentic proving 系统中。
6月30日 ⌄ 星期四 · 1 条
02:54
Google Research / arXiv 精选 AI 评分 94 ☆ Google Research 发布 Minerva：在 PaLM 基础上继续训练科学论文与包含数学表达式的技术网页，使模型能够直接读取自然语言数学/科学问题并生成带 LaTeX 的 step-by-step solutions。论文报告 MATH 50.3%、MMLU-STEM 75%、OCWCourses 30.8%、GSM8K 78.5%，并在 200 多个本科级 physics、biology、chemistry、economics 等 quantitative problems 上正确回答近三分之一。
评测与数据
推荐理由：Minerva 是 natural-language quantitative reasoning 的早期 scaling milestone：它证明通用 Transformer 架构只通过高质量技术语料继续训练，就能在数学和科学定量推理上取得大幅跃迁，无需外部 symbolic tools。
5月26日 ⌄ 星期四 · 1 条
01:01
arXiv / NeurIPS 精选 AI 评分 88 ☆ NaturalProver 研究自然数学语言中的 next-step suggestion 与 full proof generation，并让模型显式条件化于 theorem / definition 等 background references，可由检索或人类提供。论文在人类评测中优于 fine-tuned GPT-3；系统能够生成部分 2–6 步短证明，next-step suggestions 被大学数学学生评为正确且有用的比例超过 40%。
定理证明
推荐理由：它建立了自然语言 theorem proving 的 reference-grounded 路线：模型不只自由生成证明，而是显式绑定 definitions / theorems，并把检索结果作为 proof generation 的上下文。
5月25日 ⌄ 星期三 · 1 条
17:53
arXiv / Google Research 精选 AI 评分 95 ☆ Wu 等用 few-shot prompting 让大型语言模型把自然语言数学题自动翻译成 Isabelle/HOL formal specifications。论文报告 25.3% 的 sampled competition problems 可被完美形式化，并把这些 autoformalized statements 作为额外训练数据，将 miniF2F proof rate 从 29.6% 提升到 35.2%。
形式化数学
推荐理由：这是 LLM autoformalization 的奠基性事件之一：自然语言→formal statement 不再只是手工翻译，而成为可规模化建模与数据生成任务，并首次证明其能直接提升 downstream theorem proving。
5月24日 ⌄ 星期二 · 1 条
01:49
Meta AI / arXiv 精选 AI 评分 92 ☆ Meta AI 等提出 HyperTree Proof Search（HTPS），一种受 AlphaZero 启发的 neural theorem-proving search algorithm，并配套 online training：模型从此前 proof search 的成败中继续学习。论文报告在 held-out Metamath theorems 上，HTPS 从 65.4% 提升到 online-training 后的 82.6%；在 Lean-based miniF2F-curriculum 上将当时 state of the art 从 31% 提高到 42%。
定理证明
推荐理由：HTPS 将 tree search、verified reward 与 online learning 系统性结合到 theorem proving 中，是后来 reinforcement-learning formal prover 与 test-time search 的重要方法前身。
5月23日 ⌄ 星期一 · 1 条
02:03
arXiv / NeurIPS 精选 AI 评分 90 ☆ Thor 针对语言模型难以在大型 theorem library 中选择相关 premises 的问题，把 premise selection 委托给传统 automated theorem prover 的 hammer，其余 proof decisions 交给语言模型。论文报告 PISA success rate 从 39% 提升到 57%，且 8.2% 的问题是单独语言模型和单独 ATP 都无法解决、但组合系统能解决的。
定理证明
推荐理由：它把 neural generation 与 symbolic retrieval / automation 显式分工，是后续 retrieval-augmented theorem proving、tool-using agents 和 hybrid formal systems 的早期代表架构。
2月3日 ⌄ 星期四 · 1 条
08:17
arXiv / OpenAI 精选 AI 评分 91 ☆ Polu 等研究 language-model-based formal mathematics 中的 expert iteration：证明搜索与学习交替进行，模型把自己找到的 proofs 加入训练数据，并在多样化 formal statements 上逐步发现更难问题。论文显示这种自生成 curriculum 在相同 compute 下显著优于纯 proof search，并在 miniF2F 上达到当时 state of the art。
定理证明
推荐理由：这项工作很早就建立了后来反复出现的 formal-math data flywheel：search → verified proofs → retraining → harder search，而且不要求每个 training statement 预先配有人工 proof。