Prover Agent: An Agent-based Framework for Formal Mathematical Proofs
https://arxiv.org/abs/2506.19923
>We present Prover Agent, a novel AI agent for automated theorem proving that integrates large language models (LLMs) with a formal proof assistant, Lean. Prover Agent coordinates an informal reasoning LLM, a formal prover model, and feedback from Lean while also generating auxiliary lemmas to assist in discovering the overall proof strategy. It achieves an 86.1% success rate on the MiniF2F benchmark, establishing a new state-of-the-art among methods using small language models (SLMs) with a much lower sample budget than previous approaches. We also present case studies illustrating how these generated lemmas contribute to solving challenging problems.
informal reasoning LLM (8B DSR1Qwen3), a formal prover model (7B DSPv2), and the Lean verification system (7B Kimina Autoformalizer).
https://github.com/kAIto47802
Code might be posted here but no specific repo was linked.