一、概念内涵

定理证明自动化是人类文明一直以来的梦想和不懈的追求。AI驱动的形式化证明生成，是指利用大语言模型（LLM）的推理与生成能力，自动产出可由交互式定理证明助手（如Lean、Coq、Isabelle等）严格验证的形式化证明代码的新范式。传统上，形式化证明的编写需要数学家或工程师精通形式化语言和证明策略，是一项极其耗时且门槛极高的工作。大模型的介入使这一过程发生了根本性变革：LLM作为“创意引擎”生成证明策略与代码草图，交互式定理证明助手作为“验证官”对每一步进行逻辑检查——形式化证明的正确性可以得到严格验证，不存在幻觉的可能。二者通过“生成—验证—修正”的闭环迭代协作，既保留了大模型的灵活性与创造力，又继承了形式化系统的严谨性与可靠性，使AI从“能猜”走向“能证”、从“黑箱”走向“透明”。这一联姻正在重新定义数学研究与软件验证中人与机器的分工。

二、研究热点

1、“生成—验证”闭环智能体的规模化突破

将大语言模型作为证明生成器、Lean等交互式定理证明助手作为验证引擎的闭环智能体，是当前最活跃的研究方向。传统的做法是让LLM反复生成证明，有时多达数千次，直到某一次通过验证。新一代智能体框架则通过更精巧的协作机制大幅提升了效率。 这方面的代表性工作包括Goedel-Prover-V2、Rethlas智能体、Numina-Lean-Agent等。

·Goedel-Prover-V2由普林斯顿大学与清华大学等机构合作研制，通过分层式数据合成与Lean证明助手反馈迭代修正，在多个基准上取得了领先表现（https://arxiv.org/pdf/2508.03613）。

·Rethlas智能体的核心工作机制是“生成—验证”的双智能体架构。它包含一个生成智能体和一个验证智能体。生成智能体会像人类数学家一样，利用名为Matlas的数学定理搜索引擎，在海量数学文献中探索策略、寻找线索并构建候选证明。而验证智能体Archon则负责审核这些候选证明，通过其专用的LeanSearch引擎，将它们转化为Lean 4形式化语言，并自主填补证明中的逻辑缺口，进行机器可验证的严格检查。通过这两个智能体不断迭代的“生成—验证”循环，系统能逐步修补漏洞并最终找到一个可靠的证明。Rethlas智能体在完全没有人类参与的条件下，自主解决了交换代数领域悬置十余年的Anderson猜想，并生成了约19,000行的Lean 4形式化证明代码。

·Numina-Lean-Agent由中国科学院数学与系统科学研究院数学机械化实验室与Numina等机构合作研制。Numina-Lean-Agent通过模型上下文协议（MCP）将Claude Code与Numina-Lean-MCP相结合，使智能体能自主与Lean形式化系统交互、检索相关定理，并调用非形式化证明等辅助推理工具。Numina-Lean-Agent成功形式化证明了2025年William Lowell Putnam数学竞赛的全部12道试题（https://arxiv.org/abs/2601.14027）。

2、自动形式化：从自然语言到机器可验证代码

自动形式化（Autoformalization）指的是将自然语言描述的数学定理和证明自动翻译为形式化语言代码。这是打通“人类可读的数学”与“机器可验证的证明”之间的关键桥梁。这方面的国内外代表性工作包括DSP/DSP+、CriticLean等。

·DSP（Draft, Sketch, and Prove）通过“起草—草图—证明”三步流水线，将非形式化证明草稿转化为形式化草图，再由定理证明器填补缺口，其升级版DSP+则对每个阶段进行了细粒度的神经符号增强。DSP+无需任何额外模型训练或微调，在miniF2F上可解决80.7%的问题，在ProofNet上达到32.8%，成功证明了此前所有工作未能解决的IMO 2019 P1，还生成了人类可理解的证明模式，借此发现了miniF2F数据集中8个错误形式化的命题，展示了神经符号协同在不依赖海量训练资源前提下依然能实现顶尖性能的巨大潜力（https://arxiv.org/abs/2210.12283）。

·CriticLean是字节跳动Seed团队与南京大学联合提出的一个创新框架，它通过将评估（批评）环节从被动的验证者提升为主动的学习组件，一举将数学自然语言到Lean 4代码的形式化准确率从38%提升至84%。该框架的核心是训练一个专门的语义评估模型CriticLeanGPT，它能精准判断生成的形式化代码是否忠实于原始数学语义，从而发现“代码编译通过但逻辑偏离原题”的隐性问题。基于此，团队还发布了用于评估模型语义区分能力的基准CriticLeanBench，以及包含超过28.5万个高质量条目的数据集FineLeanCorpus。CriticLean的成功证明了在自动形式化流程中，优化“批评阶段”对于生成可靠、语义正确的形式化代码至关重要。（https://arxiv.org/pdf/2507.06181）。

三、发展趋势

AI驱动形式证明的发展正呈现出三大核心趋势：

·一是从“解题”到“发现”的跃迁——系统已不满足于竞赛题（如IMO、Putnam），而是开始自主攻克Erdős问题、Anderson猜想、Navier-Stokes方程等悬置多年的开放问题，并主动提出新猜想，角色从验证工具向数学发现伙伴转变；

·二是从“全自动”到“人机协同”的务实转向——完全自动仍面临搜索爆炸等根本挑战，而Numina-Lean-Agent等框架通过嵌入证明助手工作流，将人类手动步骤减少近一半，形成“人类定义方向—AI大规模探索—形式系统验证—人类审查”的协作闭环；

三是从“重训练”到“轻量协同”的效率革命——DSP+无需任何训练即达到与大规模强化学习系统相当的性能，CriticLean将自动形式化准确率从38%提升至84%。综合而言，形式证明正从“大力出奇迹”走向“巧力破难题”，从孤立解题走向系统知识建构，从单点突破走向人与AI协同进化。