ByteDance-Seed/BFS-Prover

BFS-Prover is a 7.6 billion parameter tactic generation model developed by ByteDance-Seed, based on Qwen2.5-Math-7B. It is specifically designed for automatic theorem proving in Lean4, generating tactics from proof states. The model achieves state-of-the-art performance on the MiniF2F test benchmark without requiring a critic model, making it highly effective for formal verification and mathematical proof assistance.