标签
OpenAI 发布了数百个由 AI 生成的高难度数学问题解答，但这些解答未能达到数学与人工智能咨询小组的标准，在形式化、思维链披露和人类可理解性方面存在不足。剑桥大学和国王学院的一篇论文指出，自然语言证明与 Lean 代码之间存在差异。
Shopify 回归原生移动应用后，作者认为真正的转变不是性能问题，而是 AI 编码智能体让编写代码不再昂贵，从而把重心转向形式化验证等更难的工程环节。
研究者正迅速超越 OpenAI 近期由 AI 生成的数学成果，改进后的证明已通过 Lean 进行形式化验证，凸显了 AI 辅助定理证明领域的飞速进展。
OpenAI 发布了 372 项重大数学突破，其中包括带有 Lean 证书的机器生成的 Subhash Khot 唯一游戏猜想证明——这是首批人类数学家尚未理解其证明过程的成果。
OpenAI 发布了 openai/math 代码库，其中包含 722 篇手稿，归入 372 个研究脉络——涵盖整数乘法低于 n log n、π 的无理化指数以及 Mahler 猜想等成果。这些成果由一个尚未发布的内部模型在约 4,000 个问题上生成，其中许多结果已用 Lean 形式化。
Astra 和 Claude 协助证明了 11 个正方形的已知最佳装填是已知最优的，该结果已完全在 Lean 证明助手中形式化。这是 AI 辅助数学与形式化验证的又一个里程碑。
本文提出了一种双向类型切片理论：选取一个项并查询其类型信息后，可得到一个足以解释该类型的最小程序切片。该元理论已用 Agda 形式化，并为 Hazel 编程环境实现了一个线性时间的近似算法。
该论文提出了 ReRoute，一个用于科学仿真器中反事实"what-if"预测的框架。它将事实数据与部分机制知识相结合——无需受控干预数据——在 CO2 分布偏移下可将气候误差降低 18.2–31.8%。其因果识别结果已在 Lean 中通过机器验证，并应用于平流—扩散系统、耦合气候仿真以及基于 ERA5 训练的仿真器。
一位研究者称自己花了三个月时间用 Claude Code 和 Codex 攻关 Erdős 第 993 号问题（树的独立集序列的单峰性），却在今天得知 Tong Zhang 和 Wei Li 上周已发布了完整证明，同时还有两份声称可成功构建的 Lean 4 形式化代码。该结果尚未经过同行评审。
一位开发者表达了悲观的先验：任何缺少形式化验证或物理气隙隔离的软件都注定会被攻破。这一观点是对相关讨论的回应——讨论涉及某 AI 实验室在智能体隔离安全评估中失败，以及近期内核 CVE 和 KVM 逃逸漏洞的背景。
作者们提出 Choir——一个用于分布式多智能体自动形式化的开放、模块化协议，将项目拆解为基于 GitHub 的任务，并通过确定性的信任门验证机制进行审核，支持 Lean 4、Isabelle 和 Rocq；该项目包含一篇预印本以及一个由 DARPA expMath 项目资助的开源代码仓库。
该论文提出了 LeanPolish，这是一个符号化的 Lean 4 流水线，发布了超过 33k 条可验证的证明修改记录及失败尝试。研究表明，可验证监督数据可能存在搜索过程引入的伪影，而对符号化压缩步骤进行迭代改进，在 miniF2F 上优于神经混合方法，并在 PutnamBench 上适度提升了整体证明重写效果。
这是一篇面向软件工程师的教程式指南，在 Lean 定理证明器中形式化关于正则语言的一个构造性证明，逐步讲解规约、实现、归纳以及形式化证明的构成要素。文中展示了如何借助 Mathlib 中已有的定理，让开发者也能轻松形式化教科书中的自动机理论。
一个研究团队对 OpenAI 的 Lean 4 三维 Navier-Stokes 爆炸形式化证明进行了审计，发现该解在数学上虽完全成立，但在原子尺度上会物理失效（流体在 0.7 纳米处汽化）——这是一种典型的规格博弈（specification gaming）。他们提出为神经符号 AI 系统增加一个物理边界层，并开源了其验证脚本。
Hillel Wayne 解释了 TLA+ 能验证哪些性质（安全不变式、动作性质、活性），以及仍存在哪些局限。在 Boris Cherny 提到 Claude 的 Opus 曾用 TLA+ 找出竞态条件之后，这篇文章为形式化方法的热度降降温。
团队在他们的代理集群中使用了 TLA+，实现了 99.998% 的状态可能性减少，并解决了 10 个难以发现的性能问题。
使用AI辅助方法证明了ζ(5)的无理性，该解决方案在FrontierMath上被标记为已解决，尽管它没有采用最初预期的Apéry风格证明。
这篇论文提出了一个用于评估数学定理内在趣味性的度量标准，并训练了一个27B模型来预测证明难度，从而能够生成更有趣和新颖的数学成果，同时减少与现有知识库的重叠。
本文介绍了一个框架，使LLMs能够发现和证明有趣的数学定理，通过优化基于证明难度的指标，从而产生更多新颖且有用的数学知识，并减少与现有库的重叠。
本文介绍了一种在Lean中利用LLMs自动生成具有完备性形式化证明的泛化规划的方法，并在基准领域上进行了评估，展示了在自动规划验证方面的显著进步。