<?xml version="1.0" encoding="UTF-8"?>
<modsCollection xmlns="http://www.loc.gov/mods/v3">
<mods ID="khrulev-2026-blueprintrepair">
    <titleInfo>
        <title>BlueprintRepair: Typed Local Edits for Failed Lean Proof Blueprints</title>
    </titleInfo>
    <name type="personal">
        <namePart type="given">Ruslan</namePart>
        <namePart type="family">Khrulev</namePart>
        <role>
            <roleTerm authority="marcrelator" type="text">author</roleTerm>
        </role>
    </name>
    <originInfo>
        <dateIssued>2026-10</dateIssued>
    </originInfo>
    <typeOfResource>text</typeOfResource>
    <relatedItem type="host">
        <titleInfo>
            <title>The Proceedings of the 4th Workshop on Mathematical Natural Language Processing (MathNLP 2026)</title>
        </titleInfo>
        <name type="personal">
            <namePart type="given">Marco</namePart>
            <namePart type="family">Valentino</namePart>
            <role>
                <roleTerm authority="marcrelator" type="text">editor</roleTerm>
            </role>
        </name>
        <name type="personal">
            <namePart type="given">Deborah</namePart>
            <namePart type="family">Ferreira</namePart>
            <role>
                <roleTerm authority="marcrelator" type="text">editor</roleTerm>
            </role>
        </name>
        <name type="personal">
            <namePart type="given">Mokanarangan</namePart>
            <namePart type="family">Thayaparan</namePart>
            <role>
                <roleTerm authority="marcrelator" type="text">editor</roleTerm>
            </role>
        </name>
        <name type="personal">
            <namePart type="given">Leonardo</namePart>
            <namePart type="family">Ranaldi</namePart>
            <role>
                <roleTerm authority="marcrelator" type="text">editor</roleTerm>
            </role>
        </name>
        <name type="personal">
            <namePart type="given">Jo-Ku</namePart>
            <namePart type="family">Cheng</namePart>
            <role>
                <roleTerm authority="marcrelator" type="text">editor</roleTerm>
            </role>
        </name>
        <name type="personal">
            <namePart type="given">Andre</namePart>
            <namePart type="family">Freitas</namePart>
            <role>
                <roleTerm authority="marcrelator" type="text">editor</roleTerm>
            </role>
        </name>
        <originInfo>
            <publisher>Association for Computational Linguistics</publisher>
            <place>
                <placeTerm type="text">Budapest, Hungary</placeTerm>
            </place>
        </originInfo>
        <genre authority="marcgt">conference publication</genre>
        <identifier type="isbn">979-8-89176-468-2</identifier>
    </relatedItem>
    <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 release 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.30\times as expensive, rewriting 2.06\times), and within 10000 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. Code, benchmark, and trajectories are available at https://github.com/Karifannaa/BlueprintRepair.</abstract>
    <identifier type="citekey">khrulev-2026-blueprintrepair</identifier>
    <location>
        <url>https://aclanthology.org/2026.mathnlp-main.3/</url>
    </location>
    <part>
        <date>2026-10</date>
        <extent unit="page">
            <start>30</start>
            <end>41</end>
        </extent>
    </part>
</mods>
</modsCollection>

%0 Conference Proceedings
%T BlueprintRepair: Typed Local Edits for Failed Lean Proof Blueprints
%A Khrulev, Ruslan
%Y Valentino, Marco
%Y Ferreira, Deborah
%Y Thayaparan, Mokanarangan
%Y Ranaldi, Leonardo
%Y Cheng, Jo-Ku
%Y Freitas, Andre
%S The Proceedings of the 4th Workshop on Mathematical Natural Language Processing (MathNLP 2026)
%D 2026
%8 October
%I Association for Computational Linguistics
%C Budapest, Hungary
%@ 979-8-89176-468-2
%F khrulev-2026-blueprintrepair
%X 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 release 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.30\times as expensive, rewriting 2.06\times), and within 10000 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. Code, benchmark, and trajectories are available at https://github.com/Karifannaa/BlueprintRepair.
%U https://aclanthology.org/2026.mathnlp-main.3/
%P 30-41

Markdown (Informal)

[BlueprintRepair: Typed Local Edits for Failed Lean Proof Blueprints](https://aclanthology.org/2026.mathnlp-main.3/) (Khrulev, MathNLP 2026)

• BlueprintRepair: Typed Local Edits for Failed Lean Proof Blueprints (Khrulev, MathNLP 2026)

ACL

• Ruslan Khrulev. 2026. BlueprintRepair: Typed Local Edits for Failed Lean Proof Blueprints. In The Proceedings of the 4th Workshop on Mathematical Natural Language Processing (MathNLP 2026), pages 30–41, Budapest, Hungary. Association for Computational Linguistics.