https://zeyu-zheng.github.io
-
BFS-Prover-V2-32B
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.
8 Pulls 3 Tags Updated 1 week ago
-
BFS-Prover-V1-7B
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.
7 Pulls 3 Tags Updated 3 weeks ago
-
BFS-Prover-V2-7B
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.
3 Pulls 3 Tags Updated 3 days ago