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

A new pipeline called BASE reduces the computational cost of using the Lean proof assistant to verify mathematical reasoning by roughly a factor of five, while simultaneously improving answer-selection accuracy, according to a paper posted to arXiv on 14 June 2026 [1][2]. The approach, described by researchers as a “base-and-edit” pipeline, formalizes only a single base candidate per problem in Lean and then derives the remaining statements by editing the answer expression in place [1][2]. Lean is a proof assistant and functional programming language based on the calculus of constructions with inductive types, developed as a free and open-source project [4]. It allows machine-checkable verification of reasoning outputs, which is useful for tasks such as selecting the best answer from K sampled candidates during test-time scaling [2]. Existing methods that use Lean for answer selection call an autoformalization model to generate a formal statement for each candidate independently, which incurs significant computational cost [2]. BASE instead trains a rewriter model called LEANSCRIBE to localize the answer within the base formalization and produce a reusable edit function for the remaining K−1 candidates [1][2]. The paper reports that this design cuts autoformalizer calls by about 5x at K=8, and the reduction is expected to grow as K increases [1][2]. The researchers evaluated BASE across four benchmarks and three solvers, covering 12 distinct dataset-and-solver configurations [1][2]. They state that BASE achieves a Pareto improvement—higher selection accuracy and lower formalization cost—on all 12 configurations [1][2]. Code for the pipeline has been made available on GitHub [1][2]. The work arrives as large language models are increasingly deployed for mathematical reasoning, where formal verification tools such as Lean offer a way to check outputs with rigorous, machine-readable proofs [2]. The history of formal methods in mathematics stretches back to ancient civilizations’ contributions to astronomy and geometry, but the modern integration of proof assistants with neural reasoning systems represents a more recent development [3].