Evaluating the Robustness of Proof Autoformalization in Lean 4

Zhengtao Gui, Sheng Yang, Zhouxing Shi

Proof autoformalization aims to translate a mathematical informal proof written in natural language into a formal proof in a formal language such as Lean~4. Several works have deve…