7  Downloads Updated  3 weeks ago

BFS-Prover-V1-7B is a step-level theorem proving model for Lean4, used to predict the next tactic given a tactic state. The model is developed by the ByteDance Seed team.