Ruslan Khrulev

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 ch...