8  Downloads Updated  1 week ago

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