Efficient proof generation method finds multiple answers simultaneously
Efficient Proof Generation for Lean Statements with Multiple Candidate Answers
Computation and LanguageArtificial IntelligenceMachine Learning
Summary
Sometimes when people use math software like Lean 4 to solve math problems, the software tries many answers one at a time and checks proofs for each, which can waste time. The authors created a smarter method that looks at many possible answers together and tries to prove at least one in a single step. This saves a lot of computing work and can also spot when the math problem isn’t clearly defined because it finds multiple conflicting proofs. Their approach works well on several math problem sets and is available online.
What this means in practice
- •For formal methods engineers: Reduce computing time in verifying multiple candidate solutions by generating proofs for many answers in one step.
- •For educational technology developers: Detect ambiguous or incorrectly posed math problems by identifying multiple conflicting formal proofs automatically.
Authors
Pengzhen Lin, Ke Zhang, Maziar Raissi, Zhouxing Shi
Abstract
In formal systems such as Lean 4, efficiently finding answers to mathematical problems and generating verifiable proofs is an important task in automated mathematical reasoning. In the traditional way where an upstream solver provides multiple candidate answers, the common workflow requires searching for proofs for each candidate separately, incurring redundant computational cost. To this end, we propose a joint proof framework that integrates candidate answer selection, answer supplementation, and formal proof generation into a unified reasoning process. At its core is a trained prover that selects given or proposes new answers and generates a proof for at least one answer in a single call. Joint proof can also reuse generated proofs to check for faithfulness errors. For problems with a unique answer, if two distinct answers both obtain verifiable proofs under the same formal statement, this confirms the statement does not faithfully preserve the original problem semantics. On MATH-500, AMC 2023, and AIME 2024/2025/2026, our framework achieves the same formal proof success rate as per-candidate proof generation with about one sixth of the token cost, and identifies at least 6.1% of the formalized statements as unfaithful without requiring additional judges. Our model and code are available at https://github.com/Linppz/Gobble-Prover.