Proving（证明）在 AI 领域主要指让模型生成可被机器验证的数学或程序正确性证明，目前正处于从学术研究走向工程落地的关键阶段。与传统生成式 AI 输出无法保证正确不同，证明类任务的结果可以被形式化系统（如 Lean 4）逐条检查，因此被视为衡量 AI 推理能力、并解决“AI 代码不可信”问题的核心路径之一。
定理证明的近期进展
围绕形式化定理证明，近期出现了多条研究路线：Lean Graph Search for Formal Theorem Proving 探索以图搜索方式在 Lean 中寻找证明路径；IneqAgent: Agentic Inequality Proving in Lean with Symbolic Computation 将智能体式不等式证明与符号计算结合；SCOPE: Certified Theorem Proving with a Language Model as the Policy Planner 则让语言模型充当策略规划器，产出可认证的证明。值得注意的是，NanoProof: Open and Efficient Automated Theorem Proving in Lean 4 主打开源与高效，反映出该方向正从“追求最强模型”转向“轻量可用”的工程化竞争。
Proving 从数学走向代码审查
证明能力不只停留在数学题上，也在重塑软件工程。Addy Osmani 在讨论 Agent 时代代码审查时提到一个数据点：Claude 编写了 Claude Code 约 90% 的代码，而在 6 月到 9 月间，团队合并的 PR 数量翻倍以上，回滚率反而下降（Addy Osmani 谈 Agent 时代代码审查的重构）。这一现象背后的逻辑正是用更强的验证与审查机制替代人工把关。社区工具层面，pstack 新增了 /create-formal-verification-skill，定位为 meta-skill：不直接执行形式化验证，而是根据系统特性自动生成对应的验证技能，说明验证工作流本身也在被自动化。
当前焦点与观察点
当前的争议焦点在于：其一，Proving 的适用边界——数学不等式、定理库证明已有可复现路线，但大规模工业软件的形式化验证成本仍高，meta-skill 式的自动生成能否降低门槛值得跟踪；其二，评价标准——经过验证的证明可以完全可信，但“模型给出证明思路、搜索算法补全细节”的分工模式中，各环节贡献如何衡量尚无共识；其三，开源轻量模型（如 NanoProof）与闭源大模型在该任务上的差距是否在收窄。总体来看，可机器验证的输出正在成为 AI 可靠性叙事的重要支点，后续观察重点是其从 Lean 社区向通用代码正确性保障扩散的速度。