AI RESEARCH
Surface Sensitivity in Lean 4 Autoformalization
arXiv CS.LG
•
ArXi:2604.23135v1 Announce Type: new Natural-language variation poses a key challenge in Lean autoformalization: semantically equivalent paraphrases of the same theorem statements can induce divergent formal outputs, yet it remains unclear whether this variation reflects semantic disagreements or shallower failures. We investigate this question in Lean 4 using 60 deterministic paraphrase rules applied to ProofNet\# and miniF2F.