Counterexample-Carrying FormalRx: Lean-Checkable Witnesses for Autoformalization Misalignment

Autoformalization systems can write Lean statements that compile but mistranslate the original mathematics. Existing diagnostic benchmarks like FormalRx ask the model to label and repair the mismatch, but a correction alone does not prove that the candidate and intended formalizations differ in meaning. Lean checks the proposition it sees, not whether the English was captured. We propose Counterexample-Carrying FormalRx (FormalRx-CC): every misalignment diagnosis must be accompanied by a small Lean-checkable artifact that mechanically separates the candidate from the intended formalization. We give a task definition, a seven-family witness taxonomy, an adversarial verification protocol that rejects sorry, admit, and escape hatches, and a 204-example executable artifact with completed 204-example runs on GPT-4.1-mini, GPT-4.1, and Claude Haiku plus one-pass Lean-feedback repair. The results expose a distinction that single-number scoring hides. Lean-feedback repair lifts raw Lean acceptance by 23-61% across the three models, but the joint metric that additionally requires the correct semantic direction is only 13/204 in the strict GPT-4.1-mini funnel: repair fixes proof engineering, not semantic understanding. In the GPT-4.1-mini comparison, full mode passes Lean more often than gold-target mode: 33/204 raw and 48/204 after one repair pass, versus 21/204 in gold mode, suggesting that raw Lean success can conflate witness construction with self-target selection.