Efficient Proof Generation for Lean Statements with Multiple Candidate Answers.

arXiv:2610.34490v1 Announce Type: cross 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