修Lean证明蓝图？这个接口用类型化编辑，比源码补丁省30%、比重写省一半，1万token内就顶到上限。
BlueprintRepair是一种让大模型通过十种受模式检查的局部操作修改Lean证明蓝图的修复接口。研究构造了包含142个受控失败案例的BlueprintTrace基准，并对比了类型化编辑、精确源码补丁和完整模块重写三种方式。在DeepSeek-V4-Flash下，三种接口解决的局部失败数几乎相同，但类型化修复每个已解状态成本最低，补丁费用为其1.30倍，重写为其2.06倍。在每任务10000个补全token预算内，类型化修复几乎达到最终覆盖率，而两种自由形式接口明显落后。Qwen3.6-Flash解决的案例更少，但类型化修复依然最便宜，并在证明编写类状态上领先。
BlueprintRepair: Typed Local Edits for Failed Lean Proof Blueprints
LLM-based Lean proving systems increasingly organize a proof as a blueprint: a dependency graph of formal statements. We introduce BlueprintRepair, a repair interface that lets a model change this graph through ten schema-checked local operations. An operation names the node it edits, so the target theorem cannot be changed. Lean checks every applied change, and an accepted repair must declare every blueprint lemma its proof uses. We also construct BlueprintTrace, a benchmark of 142 controlled failures with complete accepted and rejected repair trajectories. We compare typed edits, exact source patches, and complete module rewrites under matched source, feedback, model, and budget, one episode per state and interface. With DeepSeek-V4-Flash, the three interfaces solve almost the same number of the benchmark's localized failures. Typed repair is the cheapest per solved state (patching is 1.30x as expensive, rewriting 2.06x), and within 10,000 completion tokens per task it reaches almost all of its final coverage, while both free-form interfaces are well behind. A second model, Qwen3.6-Flash, solves fewer states but keeps typed repair cheapest, puts it ahead on the proof-authoring states, and repeats the localized pattern.