Evaluating the Robustness of Proof Autoformalization in Lean 4.

arXiv:2606.14867v3 Announce Type: replace-cross Abstract: Proof autoformalization aims to translate a mathematical informal proof in natural language into a formal proof in a formal language such as Lean 4. Existing LLM-based models for proof autoformalization