Formalize Once, Edit the Rest: Efficient Lean-Based Answer Selection for Math Reasoning

Ji Feng, Zhouxing Shi

With large language models (LLMs) increasingly applied to mathematical reasoning, formal proof assistants such as Lean can be leveraged to verify reasoning outputs with machine-che…