在依赖项目上下文的Lean 4定理证明中，失败证明过去被当作最终筛选结果丢弃，独立采样让后续尝试几乎从头开始。这套搜索框架让通用推理模型与Lean专用证明器各出一个候选，用编译器错误做两两比较选出当前最佳证明，只在比较判定更好时接受修订，停滞则重新采样。在miniCTX-v2的七个真实Lean 4项目上，pass@32预算内平均通过率比两个基座模型的平均pass@32高12.8个百分点，LLM调用减少21.9%。
失败证明不再被直接丢弃，而是成为后续搜索的起点：系统始终维护一个当前最佳证明状态，围绕它修订，并在停滞时换起点。 此前的独立采样把编译器当作最终过滤器，只统计k个候选中是否有任何一个通过验证，失败证明即使含有项目专用引理或接近正确的策略序列也被丢弃。 在miniCTX-v2的七个真实Lean 4项目上，pass@32预算内平均通过率比两个基座模型的平均pass@32高12.8个百分点，同时LLM调用减少21.9%。
探索阶段由两个互补模型各生成一个候选，一个擅长读长项目上下文，一个擅长Lean语法与策略。 单一模型反复采样往往重复同类错误，两个模型给出的失败方式不同，因而起点更多样。 在391次两模型都产出候选的比较中，GPT-5-mini被选中58.6%，DeepSeek-Prover-V2仍被选中41.4%，说明专用模型提供了互补候选。
修订不再无条件覆盖当前证明，而是先提出再接受：由LLM裁判连同编译器错误比较新旧两份证明，只有判定新证明更可能成功才替换。 标准迭代修订把每次修订都当作状态更新，即使新证明修好一个错误又引入另一个，错误会逐轮累积并把搜索推离正确证明。 在成功的修订轨迹上，平均约50.4%的修订提案被拒绝；在最终验证前经过比较步骤的已解轨迹中，39.5%是裁判保留了原有当前最佳证明而非接受最新提案后通过验证的。
当连续N轮修订被拒、当前路径不再改善时，系统回到探索，从两个模型重新取候选，而不是只从产生停滞证明的那个模型重采。 两两比较能保住有希望的证明状态，却无法跳出根本走错的证明策略，重新采样是这种情况下的退路。 在mathlib-valid上，停滞阈值取K/4时通过率60.00%、平均24.42次LLM调用，优于K/12、K/6、K/3、K/2四档设置。
演示范围是miniCTX-v2的七个真实Lean 4项目测试划分与RLMEval-FLT3的84个定理（easy设置，项目引理全部可用），方法在整证明层面生成、修订与比较完整证明，不做策略级搜索。
比较由LLM裁判完成，原文指出它灵活但不一定总反映真实证明进展；框架在推理时使用预训练模型，未通过多轮Lean反馈训练模型；主结果按每种方法与预算单次运行报告。
