49  Downloads Updated  1 month 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.