ByteDance-Seed/BFS-Prover-V2-7B

BFS-Prover-V2-7B by ByteDance-Seed is a 7.6 billion parameter step-level theorem proving system for Lean4, built upon the Qwen2.5-Math-7B base model. It utilizes a multi-stage expert iteration framework and best-first tree search for training, and is designed to generate Lean4 tactics from given tactic states. This model achieves strong performance on theorem proving benchmarks like miniF2F, making it suitable for automated theorem proving and formal verification tasks.