Beyond Compilation: Evaluating Faithful Natural-Language-to-Lean Statement Formalization.

arXiv:2606.31002v4 Announce Type: replace Abstract: Lean verifies that a generated declaration is well typed, but cannot check whether it states what the user intended. We measure how far compilation overstates faithfulness in statement autoformalization witho