神经网络找到高幅水波候选解，区间算术与Lean把残差界变成可核验的数学陈述
物理信息神经网络此前只能给出采样点上的小残差，无法说明连续域上的误差有多大。这条流程让网络在共形坐标的Babenko方程上搜索高幅重力—毛细波，经多级神经修正、傅里叶投影与牛顿抛光把最大采样残差降低约七个数量级，再把候选冻结为显式三角多项式，用区间算术给出连续残差的严格一致上界，并在Lean中机器核验从数值界到最终残差定理的推导。
千个智能体自己分工重证费马大定理：28.7小时、输出词元仅为原版三分之一
Anthropic 让 1000 个运行 Claude Fable 5.2 早期版本的智能体，在没有 Prove2Me 平台、也没有研究员指挥的条件下，仅凭 Git 和共享 SQL 数据库重做了费马大定理的形式化证明。团队用 28.7 小时完成，输出词元约为此前由研究员加数十个智能体、耗时 11 天完成的那次形式化的三分之一，写出的证明长度约为原来的七分之一。这是一次玩具实验，作者称它说明此类智能体团队能在精心设计的安全边界内完成长周期目标。
Axiom把7500页Stacks Project搬进Lean：代数几何基础成为可导入的机器校验库
Axiom发布Stacks Project的Lean形式化版本，把这部约7500页、奠定现代代数几何基础的开放参考书变成单一机器校验库，规模约1600万行代码。此前代数几何缺少对应的Lean基础设施，一个新证明往往要先串起交换代数、概形、层、上同调与代数栈的长链定理。该库保留原文永久标签，使研究者与AI智能体可直接导入定义和定理，并在形式化过程中定位到若干需要补假设或修正的陈述。
VeriBase把验证成功的代码与定理一起泛化：通用库让任务成功率从63.0%升到73.0%
软件验证的证明往往比写代码更费力，而已完成的验证成果很难自动变成可复用定理库。VeriBase把代码与其关联定理当作一个声明族，经证明、泛化、收割三个阶段自动构建Lean库，并在接口变化时同步更新依赖声明。由4,191个独立程序构建的通用库把三个单文件基准、三个后端模型上的平均任务成功率从63.0%提升到73.0%，平均完成时间缩短13.2%。
证书不再只靠数值求解器：LLM2Cert 把 105 个动力系统里的 81 个验到核验通过
动力系统的稳定性与安全性通常靠 Lyapunov 函数和屏障证书给出保证，而以往验证这些候选证书的数值求解器、区间方法和 SMT 求解器往往需要放宽条件，标准测试集也因此偏向低维多项式系统。LLM2Cert 让大模型提出候选证书，把每条证明义务按类型分派给 SMT 求解器或 Lean 证明助手，并只允许修补证明、不允许改动定理。在包含 105 个实例的 DynaCertBench 上，完整框架端到端验证了 81 个实例，而单次提议不做反馈时为 63 个。
Lean证明失败不再丢弃：编译器反馈加双模型搜索，pass@32预算内平均通过率提高12.8个百分点
在依赖项目上下文的Lean 4定理证明中，失败证明过去被当作最终筛选结果丢弃，独立采样让后续尝试几乎从头开始。这套搜索框架让通用推理模型与Lean专用证明器各出一个候选，用编译器错误做两两比较选出当前最佳证明，只在比较判定更好时接受修订，停滞则重新采样。在miniCTX-v2的七个真实Lean 4项目上，pass@32预算内平均通过率比两个基座模型的平均pass@32高12.8个百分点，LLM调用减少21.9%。
大模型写Lean证明，353个Erdős开放问题自主解出9个，单题数百美元
AlphaProof Nexus把大模型生成与Lean编译器逐步校验接成智能体循环，在353个开放Erdős问题上自主解出9个，其中两题已悬置56年，单题推理成本约数百美元。
自荐式方法选择让形式化证明器在Putnam上命中率从84.2%升至95.0%
该工作把形式化证明中的方法选择重新表述为适用性判断问题，提出“自荐”机制：在一次批量调用中让库中每个方法合约针对当前目标提出它要处理的目标片段、要执行的动作及所需条件，再对含糊或无依据的提案降级排序；在Putnam 2015–2025上hit@5达95.0%，最强重排基线为84.2%，IMO ProofBench上为91.7%对88.3%。
Schneider 以 Navier-Stokes 有限时间爆破证明为例，论证 AI 预测只有在可审计的因果链中才能被信任
Tapio Schneider 以 OpenAI 于 9 月 8 日宣布的强制 Navier-Stokes 方程有限时间爆破证明为切入点，区分了作为解释性理解的 episteme 与作为预测技艺的 techne，主张当预测必须在被经验验证之前就被信任时（如数十年气候预估、新构型飞机设计），信任来自从假设与输入数据到结果的、每一环都可单独检验的可审计因果链，因此 AI 应嵌入守恒律等可审计脚手架中，用于学习可被高分辨率模拟、观测或实验检验的闭合模型，而不是采用端到端模型。
Lean Pool：由 AI 代理维护的形式化数学档案库
Lean Pool 是一个由 AI 代理生长、维护与优化的形式化数学仓库，论文报告其截至 2026 年 9 月 21 日已汇集 211 个已完成项目、3,228,485 行 Lean 代码、18 位提交贡献者，并通过代理辅助的依赖升级、证明压缩与数学评审来维持这些独立开发的形式化成果在 Lean/Mathlib 演进中持续可用。
已读完全部报道