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.

Lifelong knowledge-editing benchmarks turn changes in a structured knowledge base into natural-language edits and evaluation questions. Their value depends on that conversion preserving what each fact says and which entity it concerns. We audit WikiBigEdit, a benchmark of more than 500,000 Wikidata updates, and trace its released construction pipeline to a string scan over a text rendering of Wikidata rather than a parse of its data model. From a uniform random sample of 1,500 rows, we audit the 1,458 resolvable rows against their source revisions and find three consequences: qualifier and reference values are promoted to main facts; 23.1% of resolvable rows attach correct answer text to the wrong entity identifier; and locality probes are chosen by surface-string similarity rather than semantic relatedness. Overall, 22.8% of resolvable rows carry unusable text supervision. In a matched reconstruction that holds the relation and question template fixed, similarity-selected probes show 7–12 percentage points more edit-target leakage, that is, the edited answer surfaces in a neighboring question. This effect persists under parameter editing with ROME, while the aggregate locality score remains unchanged. WikiBigEdit’s official metric does not fully register the leakage. We validate the audit with an independent parser and release the audit code and a provenance-bearing repair set. Our results do not show that published scores are incorrect; they identify structural errors those scores were not designed to detect.

Final-answer accuracy hides where a mathematical solution first becomes inconsistent and whether a later correction merely masks that error. We present StateScope, an interactive system for detecting, localizing, and repairing solution-state drift: divergence between a solver’s evolving state and a symbolically verified reference trajectory. Under a controlled comparison, two solvers receive the same Computer Algebra System (CAS)-derived operation schedule and typed arguments. We provide two systems, 1) System C records the model’s textual state claim, 2) System D re-derives state in an external typed ledger. A SymPy oracle checks every transition and explains component-level differences without an LLM judge. Users can step through a run, edit an operation at any retained step, directly repair System C’s claimed state, continue the model, and repeatedly branch from earlier interventions. Our paired evaluation covers 250 problems and twelve open and proprietary models, and a human study measures diagnostic accuracy and time. StateScope targets reasoning researchers, model developers, and educators who need to inspect and manipulate more than a final answer.