Coq 证明循环：四个节点的设计

本文细化《最终方案》中的证明循环。Agent 查资料、制定计划、写代码和分析错误；Coq 执行和检查；程序保存进度、安排尝试和记录花费。

流程：检索与规划 → 生成候选 → Coq 执行 → 继续、修复或退回。证明完成后，放回原项目重新检查。

1. 检索与规划

1. 从当前目标、已知条件和定义中提取类型、函数和关系；有报错时，补充涉及的名称和类型差异，明确要找的结论。
2. 按名称或命题结构查本地结论；按数学内容查外部证明。核对定义、前提和当前是否可用。
3. 写清接下来的步骤、需要的结论和待补的证明，先检查最关键的一步。
4. 最多保留两份计划，按第 5 节分配额度；自主构思和参考已有证明可以切换。

**区分计划：**按归纳方式、存在命题的取值、关键中间结论和子问题拆法区分计划，记录关键选择和受影响的步骤。仅调整名字、措辞或同一做法的代码写法时，归入原计划。

给小结论分类：

类别	判断和处理
本计划需要	记录后续使用步骤，安排证明；需要调整时替换结论或换计划。
用于探索	用于寻找思路，记录发现，再决定采用或结束探索。

让 LLM 说明使用步骤、所需条件和与原目标的连接，程序按当前计划记录依赖，再交给 Coq 检查。用途待定的先按探索处理；采用后转为计划依赖。移除小结论时，同步撤销相关代码和依赖步骤。

**执行检索：**LLM 提出查询，程序执行检索。先看当前条件，再用 Coq 的 Search 按名称、涉及的函数或命题结构查已加载的结论，用 Check 核对类型。也可调用 grep、cat 查看项目和库的源码；引用前按任务要求引入并检查。

查外部材料时，把目标或缺少的小结论写成包含对象、定义、前提和结论的数学描述，再提取数学术语检索。找到后记录出处，并核对能否转成当前 Coq 定义下的证明。

**筛选结果：**优先选择结论能用于当前目标、且所需前提已有依据的条目；缺少的前提另记待证。保留准确名称、完整命题和来源，实际应用仍由 Coq 检查。

**安排检索：**首次处理目标、核对名称或参数、补充结论时查；选择参考证明路线或寻找整体思路时查外部。每次说明要查什么、用于哪一步，材料齐备后继续。相同环境和查询复用缓存，同一缺口先限两轮。

2. 生成候选

1. 根据当前计划和 Coq 状态生成代码；同一计划可以生成多份候选。
2. 根据思路明确程度选择短代码或完整证明。每份代码记录计划和起点，分别从各自起点运行。
3. 从已确认的起点，按 Coq 解析出的完整命令逐条限时执行。每条成功后，记录源码范围及 Coq 状态或重跑方法；首条报错、超时或状态待确认时停止，保存此前连续成功的部分。
4. 有进展就继续；报错或达到尝试上限就诊断；完整证明通过后进入原项目检查。

把连续成功的完整命令登记为可恢复进度，恢复时重跑确认。收到整文件编译失败结果后，通过逐条重跑确定可恢复的位置，再继续检查后续证明。

**判断进展：**提前写清近期要完成的证明步骤，记录执行结果，以 Coq 确认该步骤完成为明确进展。连续尝试三次仍有待证内容时，进入诊断。

3. 诊断修复

1. 保留 Coq 的原始报错，单独记录 LLM 推测的原因。查看报错涉及的定义、引理和变量，核对类型、参数和使用条件；也可试运行修改后的代码，看结果是否支持模型的判断。
2. 保留前面已确认的代码、原命题和允许条件，让 LLM 提交当前小段的修改，程序检查修改范围。
3. 从同一起点执行，以原定步骤完成为修复成功；记录已完成步骤和剩余待证内容。同一失败点先限两次修复，额度用完后回退或暂停，并记录“本轮额度用尽，目标待证”。

**整理反馈：**完整日志另存。给 LLM 发送首个错误的关键原文、对应代码及片段内位置，再补查缺失信息：

内容	保留的信息
当前任务和结果	原目标、当前计划、本轮代码版本、剩余额度；分别标明 Coq 检查失败、运行超时、工具启动失败或中途崩溃。
失败位置	换算后的片段内行列位置、完整失败命令和必要的前后代码。
错误内容	保留核心报错原文、相关表达式、实际类型、要求的类型和相关条件；文件路径及原源码行列号单独记录。
出错前状态	当前还要证明的命题、可以使用的变量和假设，以及 Coq 留待后续步骤补齐的参数或表达式。
相关记录	报错涉及的定义、引理和变量的完整类型、参数和使用条件，以及已经试过的修改和结果。

**对应位置：**以本轮交给 Coq 的完整源码为准，记录发给 LLM 的片段来自哪里，将报错行列换算为片段内位置。片段删行或拼接时，保留各段对应关系；报错在片段外时，补发所在代码。位置待确认时保留原报错，并标记“待换算”。

先读取工具提供的信息；报错文字按项目使用的 Coq 版本提取，需要进一步解析的部分保留原文并标记。单独保存开头的路径和行列说明，清理终端颜色标记和同一位置的重复提示，保留错误正文中的数字、表达式、类型和条件。按 Coq 解析结果提取完整命令。

当前程序调用 coqc 编译完整文件，收集编译结果和报错文字。需要完整证明状态时，安排逐步重跑到出错前。 LLM 返回推测的原因、依据，以及要改的代码或还需查看的内容。程序检查当前状态和剩余额度，再决定下一步。

4. 回滚换计划

当前情况	决定
当前状态待确认	先恢复最近确认的位置，再判断原计划能否继续。
有具体修改，且符合局部修复范围	从原起点有限试修。
缺少资料，原计划仍可继续	回到检索，保留进度。
查询或执行表明需要改变之前的关键选择	LLM 向程序提交要改的命令、本轮代码中的位置，以及相关 Coq 报错或查询结果，说明回退理由；程序核对执行记录，恢复到该命令之前，并将建议和恢复结果记入日志。
本轮修复额度用完	试其他候选或暂停计划。
各计划均已暂停或总额度用完	保存并返回项目管理部分。

原因待确认时，从最近保存的位置逐级向前退。一起恢复代码、全部待证问题、已知条件和待补的值，确认恢复成功再继续；必要时重新启动 Coq 并重跑。

保留仍可用的已证结论和失败记录。涉及共享值的子问题一起检查；按当前计划、代码版本和尝试记录接收请求结果。

5. 额度与完成条件

• **先定总额：**每个目标设置总时间、模型调用总次数和单次 Coq 运行时限，提前留出最终检查的时间。
• **先平均分：**把剩余时间和模型调用次数平均分给现有计划。目标仍待证明时，分别安排各计划使用自己的额度尝试关键一步，再根据结果调整额度。
• **再按进展调整：**一份计划提前结束时，优先把剩余额度给已有 Coq 确认进展的计划；额度用完就暂停。检索、生成、诊断、修复、小结论和恢复都计入所属计划及目标总额，切换计划时继续累计总花费。

不同候选任选一条成功；完成所选路径的全部必要子问题。保持原命题、相关定义和允许条件，将待证结论列为任务，检查通过后加入可用结论。完整证明在原项目重新检查通过后报告成功；停止时保存成果、待证问题和恢复位置。

6. 参考论文与参考点

论文及章节	参考点
LeanDojo / ReProver §4–5	根据当前状态检索，并限制为当前可用的结论。
Draft, Sketch, and Prove §3	把自然语言证明写成明确的中间步骤，再逐步补证。
Prover Agent §3	生成并证明辅助引理，用于寻找思路和完成证明。
DeepSeek-Prover-V1.5 §3.1	保留错误前的有效代码，结合真实状态继续生成。
Seed-Prover §2.2	在不同尝试间共享已证引理，结合反馈反复修正。
PALM §4.4–4.5	按错误种类修复，失败后回退并调用证明工具。
COPRA §3	保存状态和失败动作，用反馈指导搜索与回溯。
TacticZero §2	保留备选路径，并完成所选路径内的全部必要问题。

通过项目实验验证并调整上述计划划分、额度分配、检索与回退条件和报错整理规则。