<?xml version="1.0" encoding="UTF-8"?>
<modsCollection xmlns="http://www.loc.gov/mods/v3">
<mods ID="yang-etal-2026-text">
    <titleInfo>
        <title>Same Text, Different Transitions: Action Insufficiency in Lean Provers</title>
    </titleInfo>
    <name type="personal">
        <namePart type="given">Edison</namePart>
        <namePart type="family">Yang</namePart>
        <role>
            <roleTerm authority="marcrelator" type="text">author</roleTerm>
        </role>
    </name>
    <name type="personal">
        <namePart type="given">Neel</namePart>
        <namePart type="family">Marripalapu</namePart>
        <role>
            <roleTerm authority="marcrelator" type="text">author</roleTerm>
        </role>
    </name>
    <name type="personal">
        <namePart type="given">Akshaj</namePart>
        <namePart type="family">Agadi</namePart>
        <role>
            <roleTerm authority="marcrelator" type="text">author</roleTerm>
        </role>
    </name>
    <name type="personal">
        <namePart type="given">Andrew</namePart>
        <namePart type="family">Kim</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>Neural Lean provers usually give the model only the printed text of a proof state, and some searches reuse it to decide when two states are the same. Both uses assume that states printing identically behave identically under the same tactic. We show that this assumption fails. Searching Mathlib, we find 70 verified classes of identically printed states; in 68 of them, one tactic succeeds on one member and fails on another, yielding 103 contradictory cases verified by Lean. Controlled experiments trace the difference to elaborated structure that Lean’s notation hides, and reproduce it on current Lean and Mathlib. A compact structural representation recovers the missing signal for mechanisms seen in training and fails to transfer to unseen ones. In a constructed benchmark with a known proof, merging states by identical text discards that proof in 48.4% of alias arrivals, while a structural identity prevents every loss at 8% runtime overhead. This rate is conditional on meeting an alias; in blind sampling, confirmed aliases arise at only 0.29% of search roots. Text written for people is thus not necessarily a safe identifier for machine state, and we suggest giving the model that text while identifying search states by structure.</abstract>
    <identifier type="citekey">yang-etal-2026-text</identifier>
    <location>
        <url>https://aclanthology.org/2026.mathnlp-main.18/</url>
    </location>
    <part>
        <date>2026-10</date>
        <extent unit="page">
            <start>240</start>
            <end>253</end>
        </extent>
    </part>
</mods>
</modsCollection>

%0 Conference Proceedings
%T Same Text, Different Transitions: Action Insufficiency in Lean Provers
%A Yang, Edison
%A Marripalapu, Neel
%A Agadi, Akshaj
%A Kim, Andrew
%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 yang-etal-2026-text
%X Neural Lean provers usually give the model only the printed text of a proof state, and some searches reuse it to decide when two states are the same. Both uses assume that states printing identically behave identically under the same tactic. We show that this assumption fails. Searching Mathlib, we find 70 verified classes of identically printed states; in 68 of them, one tactic succeeds on one member and fails on another, yielding 103 contradictory cases verified by Lean. Controlled experiments trace the difference to elaborated structure that Lean’s notation hides, and reproduce it on current Lean and Mathlib. A compact structural representation recovers the missing signal for mechanisms seen in training and fails to transfer to unseen ones. In a constructed benchmark with a known proof, merging states by identical text discards that proof in 48.4% of alias arrivals, while a structural identity prevents every loss at 8% runtime overhead. This rate is conditional on meeting an alias; in blind sampling, confirmed aliases arise at only 0.29% of search roots. Text written for people is thus not necessarily a safe identifier for machine state, and we suggest giving the model that text while identifying search states by structure.
%U https://aclanthology.org/2026.mathnlp-main.18/
%P 240-253

Markdown (Informal)

[Same Text, Different Transitions: Action Insufficiency in Lean Provers](https://aclanthology.org/2026.mathnlp-main.18/) (Yang et al., MathNLP 2026)

• Same Text, Different Transitions: Action Insufficiency in Lean Provers (Yang et al., MathNLP 2026)

ACL

• Edison Yang, Neel Marripalapu, Akshaj Agadi, and Andrew Kim. 2026. Same Text, Different Transitions: Action Insufficiency in Lean Provers. In The Proceedings of the 4th Workshop on Mathematical Natural Language Processing (MathNLP 2026), pages 240–253, Budapest, Hungary. Association for Computational Linguistics.