Auditing Chain-of-Thought Register Effects in Lean 4 Proof Generation

Does the register of a chain-of-thought (CoT) prompt matter when a language model writes Lean 4 proofs? We evaluate five prompt conditions on 11 models and $21,328$ analyzed model–condition–problem cells from a 500-problem LeanWorkbook draw, and report two findings that appear only once proof scoring is itself audited. First, the scoring pipeline carried two defects: the verifier read Lean's sorry warning from the wrong stream, counting unfinished proofs as successes, and the extractor handed Lean text the model never offered as its proof. Screening every stored success removes $204$ that had closed with sorry, and re-verifying the $6,548$ cells whose proof text the repair changes recovers $764$ real ones (panel successes $1,696\to 2,256$). A further $1,205$ cells were truncated before storage and cannot be re-scored; we retain their old verdicts and bound the uncertainty this creates; the adversarial bound includes no effect. Second, on the re-scored panel NL CoT alone has a panel-average interval excluding $1$ (OR $1.58$, $95\%$ HDI, a highest-density interval, $[1.14,2.10]$; raw panel rates $8.4\%\to 10.6\%$), while Lean pseudocode, symbolic math and tactic plans point above $1$ with intervals containing it. The average does not determine the effect for an untested model: heterogeneity persists ($\tau$ $0.17$–$0.47$) and the predicted interval for a new model spans $1$ in every register. After re-scoring, neither self-rewriting nor an independent renderer establishes a pooled presentation effect (OR $1.14$ $[0.91,1.43]$ and $1.02$ $[0.86,1.21]$); with five samples per problem on two models, no register's paired gain over Direct excludes zero. We report a small average benefit for one register; these data do not establish a prompting rule for an untested model.