Pith. sign in

REVIEW 3 major objections 6 minor 23 references

Typed local edits recover almost as many failed Lean proof blueprints as free-form rewrites, at far lower cost and token budget.

Reviewed by Pith at T0; open to challenge. T0 means a machine referee read the full paper against a public rubric. the ladder, T0–T4 →

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗

T0 review · grok-4.5

2026-07-31 17:32 UTC pith:22OWXOP7

load-bearing objection Solid systems paper: typed local blueprint edits match free-form coverage on localized defects and win clearly on early tokens and cost; the soft spot is external validity, not internal cracks. the 3 major comments →

arxiv 2607.28110 v1 pith:22OWXOP7 submitted 2026-07-30 cs.AI

BlueprintRepair: Typed Local Edits for Failed Lean Proof Blueprints

Ruslan Khrulev This is my paper
classification cs.AI
keywords Leanblueprint repairtyped local editsproof graphsLLM theorem provingverifier feedbackdependency checkingBlueprintTrace
verification ladder T0 review T1 audit T2 compute T3 formal T4 reserved

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

Modern LLM provers often plan a Lean proof as a blueprint: a small dependency graph of formal statements. When that plan fails, this paper asks whether the model must rewrite the whole module, or can fix the graph with a handful of typed local operations. BlueprintRepair exposes ten schema-checked edits that name the node they touch, so the target theorem cannot be silently changed; Lean verifies every step, and an accepted repair must declare every blueprint lemma its compiled proof actually uses. On BlueprintTrace, 142 controlled failures with full accepted and rejected trajectories, typed repair matches free-form patching and rewriting on localized defects while reaching nearly all of its coverage inside a 10,000-token budget and at the lowest cost per solve. A second model repeats the same efficiency pattern. The practical claim is simple: when a blueprint is mostly right, typed local edits recover most of the reachable fixes cheaply, and freer generation buys only the remainder.

Core claim

On matched runs with the same source, feedback, model, and budget, typed local blueprint edits solve nearly as many localized Lean failures as exact source patches or full module rewrites, while reaching almost all of their final coverage within 10,000 completion tokens per task and at the lowest all-in cost per solve (patching 1.30×, rewriting 2.06× with DeepSeek-V4-Flash; the same cost ordering holds for Qwen3.6-Flash).

What carries the argument

BlueprintRepair: ten schema-checked local operations on a LeanArchitect-style declaration DAG, plus a graph-aware acceptance rule that a repair is valid only if every actual proof dependency extracted from compiled terms is declared on the blueprint.

Load-bearing premise

The findings rest on small, author-built blueprints with deliberately injected defects and one episode per state, not on large real-world formalizations or multi-seed model behavior.

What would settle it

Rerun the same three-interface protocol on larger research-scale blueprints or multi-seed samples; if free-form patching or rewriting then clearly dominates both early-budget coverage and cost per solve on localized defects, the efficiency claim fails.

Watch this falsifier — get emailed when new claim-graph text bears on it.

If this is right

  • When a blueprint is mostly correct, systems can default to typed local edits and reserve free-form generation for residual hard cases.
  • Repair acceptance can and should check compiled proof terms against declared dependency edges, not only kernel success of the target.
  • Full accepted and rejected trajectories become reusable supervision for learning structural repair policies.
  • Combining interfaces in a fixed order covers more states than any single interface, with typed-first the cheapest order observed.
  • Target immutability can be enforced before an edit is applied when the action names its node.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • The same typed-edit pattern may transfer to other structured artifacts that already have a dependency graph and a verifier, such as build plans or typed IR.
  • Rejected-action reasons in BlueprintTrace are a natural source of negative examples for training repair policies without inventing synthetic faults.
  • If models were fine-tuned on the ten operations, the remaining coverage gap versus patching on localized states might shrink further without raising token cost.
  • Cost-aware routers could start every repair episode in typed mode and escalate to patch or rewrite only after a token or rejection threshold.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit.

Referee Report

3 major / 6 minor

Summary. The paper proposes BlueprintRepair, a schema-checked interface of ten local operations for editing failed Lean proof blueprints (declaration-level DAGs), together with a graph-aware acceptance criterion requiring Actual(v) ⊆ Declared(v) on compiled proof terms. It releases BlueprintTrace: 142 controlled miniF2F-based failures (91 edit-shaped, 39 proof-authoring, 12 compound) with full accepted and rejected trajectories. Under a matched protocol (same source, typed diagnostics, verifier feedback, model, step/output budget; one episode per state×interface), it compares typed edits against atomic search-and-replace patches and whole-module rewrites for DeepSeek-V4-Flash and Qwen3.6-Flash. On localized failures the three interfaces achieve near-parity coverage; typed repair is cheapest per solve and reaches nearly its full coverage by 10k completion tokens, while free-form interfaces lag on the early frontier. A hand replay shows the 11 DeepSeek patch-only solves are expressible in the typed vocabulary.

Significance. If the scoped claims hold, this is a useful systems result for LLM-based formal proving: it isolates how repair is expressed (typed graph ops vs free-form Lean) under equal information and budget, and it evaluates repaired proof graphs rather than kernel-accepted targets alone. Strengths that should be credited explicitly include the matched three-interface protocol, the Actual⊆Declared dependency gate re-checked on all stored endpoints, retention of rejected actions in BlueprintTrace, the hand demonstration that patch-only wins are not missing typed operations, McNemar intervals that avoid false-equivalence language, and a second-model replication of the cost ordering and localized near-parity. The artifact (schemas, prompts, Lean pin, trajectories, analysis scripts) makes the interface contract and predicate inspectable. Within diagnostic small-blueprint repair this is a solid contribution; transfer to research-scale or pipeline failures remains open and is largely owned in the Limitations.

major comments (3)
  1. [§4.2, Figure 3, Abstract] §4 and Fig. 3: the efficiency frontier and all-in cost-per-solve claims (typed cheapest; 103/104 solves by 10k tokens vs 90 and 87) rest on one episode per state and interface. The manuscript correctly notes this describes observed runs rather than an expectation, but the abstract and §4.2 still present precise multipliers (1.30×, 2.06×) and early-coverage counts as primary results. For a load-bearing systems comparison, either add a small multi-seed subsample (even on the 91 edit-shaped states) or reframe the abstract/conclusion so single-run status is unmistakable and variance is not implied by the point estimates.
  2. [§1 Introduction, §7 Conclusion, Abstract] §2 and Table 1–2: BlueprintTrace is author-constructed defects on intentionally small graphs (1–8 nodes, depth ≤3, only 12 compound states), with manual target selection from miniF2F. The central claim is scoped as diagnostic, yet the introduction and conclusion still invite a general systems reading (“when a blueprint is mostly correct, typed local edits recover most of the reachable coverage at the lowest cost”). Please tighten the claim language in the abstract, intro, and conclusion so it is explicitly conditional on localized, mostly-correct small blueprints, and state more clearly that the benchmark is not a sample of failures from a real generation pipeline (Limitations already says this; the front matter should match).
  3. [§4.1, Table 5] Table 5, Qwen3.6-Flash compound row: typed repair solves 4/12 compound states while patching solves 10/12—the one clear coverage break in the second model. The text reports the number but does not analyze whether multi-defect states expose a sequential one-op-per-turn disadvantage, schema friction, or model-specific tool use. Because compound failures are the closest proxy in the benchmark to non-localized repair, a short error analysis (or an explicit caveat that the efficiency story is driven by the 91 localized states) is needed so the headline “typed is cheapest and nearly as complete” is not over-read for chained defects.
minor comments (6)
  1. [Table 1, Table 7] Table 7 family counts (e.g., false/too strong n=18, missing hypothesis n=30) do not match Table 1 family sizes (23 and 34) because compounds are peeled off; a footnote on Table 1 or 7 stating the accounting rule would prevent misreading.
  2. [§4.3] The hand replay that all 11 DeepSeek patch-only solves are expressible as typed programs (§4.3) is important negative evidence against a missing-operation confound; consider a short table or appendix listing call counts per replayed repair so readers can judge budget fit without trusting a single paragraph.
  3. [Figure 3] Figure 3 price axes differ across models by design; a one-line reminder in the caption that absolute $ axes are not comparable (only within-model ordering) would help skimmers.
  4. [§2, Appendix B.2] Appendix B.2 stronger-automation baseline (3/39 closed) is valuable; a forward pointer from the proof-authoring definition in §2 would make the operational label less easy to over-interpret before the appendix.
  5. [Abstract, §1] Minor prose: “ablueprint” spacing typos appear in the abstract and opening; standardize “BlueprintRepair” / “BLUEPRINTREPAIR” casing between title, abstract, and body.
  6. [§6] Related work is appropriately focused; a brief contrast with tactic-level repair (Baldur/APOLLO) on whether those systems could satisfy Actual⊆Declared without blueprint metadata would sharpen the novelty paragraph.

Circularity Check

0 steps flagged

No significant circularity: empirical interface comparison on Lean-checked controlled failures, not a fit-or-self-cite derivation.

full rationale

BlueprintRepair is a systems paper whose load-bearing claims are coverage, token/cost frontiers, and control under a matched three-interface protocol on BlueprintTrace. Success is defined by external machine checks (module elaboration, preserved target, Actual(v)⊆Declared(v) on compiled proof terms), re-run on all stored endpoints, not by a quantity fitted from the same observations. The ten operations, acceptance predicate, and failure families are stipulated up front; results are observed episode outcomes under fixed model/budget, not predictions forced by construction. Author-built defects and small graphs are disclosed scope limits (Limitations), not a circular reduction of the efficiency claim to its inputs. Related-work citations (LeanArchitect, EditableSketch, etc.) supply motivation, not a uniqueness theorem or ansatz that forces the reported numbers. No self-definitional loop, fitted-input-as-prediction, or load-bearing self-citation chain appears in the derivation.

Axiom & Free-Parameter Ledger

3 free parameters · 4 axioms · 2 invented entities

This is an empirical systems paper. Load-bearing premises are experimental design choices and tooling assumptions, not physical axioms or fitted natural constants. No new ontological entities are postulated.

free parameters (3)
  • interaction budget (8 steps ordinary / 12 compound) and 49,152 max output tokens = 8 / 12 steps; 49152 output tokens
    Hand-chosen episode limits that define when a state is unsolved; results are conditional on these budgets.
  • fixed node-prover ladder (rfl, simp, omega; optional norm_num; 200k heartbeats) = rfl→simp→omega (+norm_num on 6 states), 200000 heartbeats
    Defines the operational split between proof-authoring and edit-shaped states and how much proof work the harness does automatically.
  • manual target selection and author-injected defect construction over miniF2F = 142 states / 141 targets
    142 states chosen and broken by the author after filtering; family balance is by design, not a random sample of natural failures.
axioms (4)
  • domain assumption Lean 4 kernel acceptance plus Actual(v) ⊆ Declared(v) on compiled proof terms is the right success criterion for blueprint repair
    Section 2 and Appendix B.1; rejects undeclared blueprint lemma use even when the target proves.
  • ad hoc to paper One episode per state and interface is sufficient to compare interfaces for the reported qualitative pattern
    Limitations explicitly notes single-episode protocol; second model is used instead of multi-seed estimation.
  • domain assumption miniF2F-derived small DAGs with injected defects are a valid diagnostic for when typed edits suffice
    Section 2 Controlled states and Limitations; not claimed to be a sample from production blueprint pipelines.
  • standard math Standard Lean/mathlib tactics and elaboration behavior are trustworthy oracles for apply/reject
    Harness applies ops and trusts Lean feedback throughout Sections 3–4.
invented entities (2)
  • BlueprintRepair ten-operation typed interface independent evidence
    purpose: Constrain LLM repairs to schema-checked local graph/proof edits with mechanical source preservation and target immutability.
    Core proposed method (Table 3); engineering interface, not a physical entity. Independent evidence is the empirical bake-off itself.
  • BlueprintTrace benchmark (142 controlled failures + trajectories) independent evidence
    purpose: Provide matched failed states and full accepted/rejected repair logs for interface comparison and future policy learning.
    Author-constructed diagnostic set; value depends on construction checks described in Section 2 and artifact claims.

pith-pipeline@v1.2.0-daily-grok45 · 18370 in / 3237 out tokens · 60995 ms · 2026-07-31T17:32:26.336671+00:00 · methodology

0 comments
read the original abstract

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.

Figures

Figures reproduced from arXiv: 2607.28110 by Ruslan Khrulev.

Figure 1
Figure 1. Figure 1: Three benchmark examples. (a) A localized defect weakens a lemma until it becomes false. (b) A compound state contains two linked defects on the target path and one disconnected node. (c) In a proof-authoring state, the graph is correct but the remaining theorem still needs proof content. Statements are abbreviated; [PITH_FULL_IMAGE:figures/full_fig_p002_1.png] view at source ↗
Figure 2
Figure 2. Figure 2: shows the complete interaction loop. The model receives the current blueprint, the current Lean source, and typed diagnostics. It emits one action in the format required by its interface. The harness applies the action, elaborates the module, runs the fixed node prover on deferred nodes, checks actual proof dependencies against declared edges, and returns a short reason for every accepted or rejected step.… view at source ↗
Figure 3
Figure 3. Figure 3: Cumulative solved states as the per-task budget increases, for both models. Panels (a) and (c) use completion tokens; panels (b) and (d) use provider price. All four use the same 142 initial states, count solved as in [PITH_FULL_IMAGE:figures/full_fig_p007_3.png] view at source ↗
Figure 4
Figure 4. Figure 4: The p40 repair. A monolithic induction goal is replaced by a base case and an induction step. The split is structurally correct, but the induction step still needs a proof. The complete five-call trajectory is: Step Operation Lean feedback / result 1 split_node refused before anything is applied: the proposed proof uses native_decide 2 split_node applied; base_case closes at once, and the proof offered for… view at source ↗

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

23 extracted references · 11 linked inside Pith

  1. [1]

    Manish Acharya, Zhenyu Liao, Yueke Zhang, Kevin Leach, Yu Huang, and Yifan Zhang. 2026. VERITAS : Verifier-guided proof search for zero-shot formal theorem proving. arXiv preprint arXiv:2606.19399

    Pith/arXiv arXiv 2026

  2. [2]

    Pawan Sasanka Ammanamanchi, Siddharth Bhat, and Stella Biderman. 2026. Faults in our formal benchmarking: Dataset defects and evaluation failures in Lean theorem proving. In Proceedings of the 43rd International Conference on Machine Learning. https://arxiv.org/abs/2606.29493

    Pith/arXiv arXiv 2026

  3. [3]

    Jui-Hui Chung, Ziyang Cai, Zihao Li, Qishuo Yin, Rohit Agarwal, Simon Park, Rodrigo Porto, Narutatsu Ri, Ziran Yang, Shange Tang, et al. 2026. Goedel-Architect: Streamlining formal theorem proving with blueprint generation and refinement. arXiv preprint arXiv:2606.06468

    Pith/arXiv arXiv 2026

  4. [4]

    Leonardo de Moura and Sebastian Ullrich. 2021. The Lean 4 theorem prover and programming language. In Automated Deduction -- CADE 28, volume 12699 of Lecture Notes in Computer Science, pages 625--635. Springer. https://doi.org/10.1007/978-3-030-79876-5_37

    doi:10.1007/978-3-030-79876-5_37 2021

  5. [5]

    DeepSeek-AI. 2026a. DeepSeek-V4: Towards highly efficient million-token context intelligence. arXiv preprint arXiv:2606.19348

    arXiv

  6. [6]

    DeepSeek-AI. 2026b. DeepSeek-V4-Flash model card. https://huggingface.co/deepseek-ai/DeepSeek-V4-Flash

  7. [7]

    Rabe, Talia Ringer, and Yuriy Brun

    Emily First, Markus N. Rabe, Talia Ringer, and Yuriy Brun. 2023. Baldur: Whole-proof generation and repair with large language models. In Proceedings of the 31st ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering, pages 1229--1241

    2023

  8. [8]

    Minsu Kim and Se-Young Yun. 2026. Process-verified reinforcement learning for theorem proving via Lean. arXiv preprint arXiv:2606.20068

    Pith/arXiv arXiv 2026

  9. [9]

    Le, Burak Gokturk, et al

    Po-Nien Kung, Linfeng Song, Dawsen Hwang, Jinsung Yoon, Chun-Liang Li, Simone Severini, Mirek Ol s \'a k, Edward Lockhart, Quoc V. Le, Burak Gokturk, et al. 2026. LEAP : Supercharging LLMs for formal mathematics with agentic frameworks. arXiv preprint arXiv:2606.03303

    Pith/arXiv arXiv 2026

  10. [10]

    David Ma, Kaijing Ma, Shawn Guo, Yunfeng Shi, Enduo Zhao, Jiajun Shi, Zhaoxiang Zhang, Gavin Cheung, Jiaheng Liu, and Zili Wang. 2026. OProver : A unified framework for agentic formal theorem proving. arXiv preprint arXiv:2605.17283

    Pith/arXiv arXiv 2026

  11. [11]

    Azim Ospanov, Farzan Farnia, and Roozbeh Yousefzadeh. 2025. APOLLO : Automated LLM and Lean collaboration for advanced formal reasoning. arXiv preprint arXiv:2505.05758

    arXiv 2025

  12. [12]

    Qwen Team. 2026. Qwen3.6-Flash model card. https://www.qwencloud.com/models/qwen3.6-flash

    2026

  13. [13]

    Z. Z. Ren, Zhihong Shao, Junxiao Song, Huajian Xin, Haocheng Wang, Wanjia Zhao, Liyue Zhang, Zhe Fu, Qihao Zhu, Dejian Yang, et al. 2025. DeepSeek-Prover-V2: Advancing formal mathematical reasoning via reinforcement learning for subgoal decomposition. arXiv preprint arXiv:2504.21801

    Pith/arXiv arXiv 2025

  14. [14]

    Talia Ringer, RanDair Porter, Nathaniel Yazdani, John Leo, and Dan Grossman. 2021. Proof repair across type equivalences. In Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation, pages 112--127

    2021

  15. [15]

    K \'a ri R \"o gnvaldsson, Chenhao Sun, Jasper Dekoninck, and Martin Vechev. 2026. Optimizing the cost-quality tradeoff of agentic theorem provers in Lean. arXiv preprint arXiv:2606.04883

    Pith/arXiv arXiv 2026

  16. [16]

    o zde G \

    Zeynel A. Ulu s an, Burak S. Akbudak, Can S. Erer, and G \"o zde G \"u l S ahin. 2026. FormalRewardBench: A benchmark for formal theorem proving reward models. arXiv preprint arXiv:2605.10141

    Pith/arXiv arXiv 2026

  17. [17]

    Evan Wang, Simon Chess, Daniel Lee, Siyuan Ge, Ajit Mallavarapu, Jarod Alper, and Vasily Ilin. 2026. Learning to repair Lean proofs from compiler feedback. arXiv preprint arXiv:2602.02990

    arXiv 2026

  18. [18]

    Zikai Xiao, Hanzheng Wang, Meng-Hao Guo, Shi-min Hu, and Shing-Tung Yau. 2026. Editable proof sketch for automated theorem proving. In Proceedings of the 43rd International Conference on Machine Learning

    2026

  19. [19]

    Swope, Alex Gu, Rahul Chalamala, Peiyang Song, Shixing Yu, Saad Godil, Ryan Prenger, and Anima Anandkumar

    Kaiyu Yang, Aidan M. Swope, Alex Gu, Rahul Chalamala, Peiyang Song, Shixing Yu, Saad Godil, Ryan Prenger, and Anima Anandkumar. 2023. LeanDojo: Theorem proving with retrieval-augmented language models. In Advances in Neural Information Processing Systems, Datasets and Benchmarks Track

    2023

  20. [20]

    Ning Zhang, Nongyu Di, Zenan Li, Yuan Yao, and Xiaoxing Ma. 2026a. Planning to hammer: Difficulty-aware decomposition for automating Rocq proofs. arXiv preprint arXiv:2606.17981

    Pith/arXiv arXiv

  21. [21]

    Lee, and Fanghui Liu

    Yuanhe Zhang, Yuekai Sun, Taiji Suzuki, Jason D. Lee, and Fanghui Liu. 2026b. LeanMarathon: Toward reliable AI co-mathematicians through long-horizon Lean autoformalization. arXiv preprint arXiv:2606.05400

    Pith/arXiv arXiv

  22. [22]

    Kunhao Zheng, Jesse Michael Han, and Stanislas Polu. 2022. miniF2F : A cross-system benchmark for formal Olympiad-level mathematics. In International Conference on Learning Representations

    2022

  23. [23]

    Thomas Zhu, Pietro Monticone, Jeremy Avigad, and Sean Welleck. 2026. LeanArchitect: Automating blueprint generation for humans and AI. arXiv preprint arXiv:2601.22554

    arXiv 2026