Prover Agent 把 informal reasoner、formal prover、Lean feedback 与自动 lemma generation 组合成低采样预算 agentic proving

Prover Agent 将自然语言 reasoning LLM、formal prover model 与 Lean feedback 协调起来，并自动生成 auxiliary lemmas 帮助形成整体 proof strategy。论文在 MiniF2F 报告 86.1% success rate，同时强调相比以往方法使用更低 sample budget，并通过 case studies 展示生成 lemma 如何帮助解决困难题。