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.