16  Downloads Updated  2 months 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.