Lean 4 是一种交互式定理证明器，旨在将数学证明编写为计算机可验证的程序，它凭借强大的类型系统和社区生态成为形式化验证领域的主流工具之一。近期，围绕 Lean 4 的 AI 辅助证明和基准测试取得显著进展，多个研究团队发布了新方法或评估框架，拓展了其在应用数学、程序验证等领域的适用性。
Lean 4 近期进展
Goedel-Architect：通过蓝图生成与精炼实现形式化定理证明新突破
该研究提出一种基于蓝图生成的定理证明方法，利用 Lean 4 的模块化特性和 AI 模型自动构建与优化证明策略，在多个数学定理上达到了更高自动化率。原文标题FVSpec：用 Lean 4 挑战真实世界属性测试的 AI 基准
FVSpec 是一个针对真实世界软件系统基本属性的测试基准，要求 AI 模型用 Lean 4 生成满足规范的形式化证明，旨在推动 Lean 4 在工程验证场景中的应用。原文标题Claude Code 在 Lean 4 程序验证中达 98.1% 成功率
实验显示，Claude Code（一种大型语言模型）在 Lean 4 的合成验证任务上取得了 98.1% 的成功率，表明当前大模型已具备辅助生成较简单 Lean 4 证明的能力。原文标题CAM-Bench：面向计算与应用数学的 Lean 4 定理证明基准
CAM-Bench 收集了覆盖数值分析、微分方程等领域的 260 个问题，为评估 Lean 4 在应用数学里的表现提供标准化测试，并能检验 AI 在科学计算形式化验证上的效果。原文标题当前焦点与观察点
AI 与 Lean 4 的结合是当前最热的方向：一方面，模型在简单证明上已接近实用，但复杂数学定理仍依赖人工干预；另一方面，多个新基准（如 FVSpec、CAM-Bench）填补了真实场景和学科交叉的评估空白，但 Lean 4 的社区库和自动化工具链仍有待完善。争议点在于，这类“AI 辅助形式化”的可靠性如何保证——模型的高成功率可能依赖特定分布，过度依赖 AI 反而增加验证成本。未来，Lean 4 或将成为 AI 推理能力的“试金石”，而学界更关注如何平衡自动化与可信度。