https://zeyu-zheng.github.io
-
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.
58 Pulls 3 Tags Updated 3 months ago
-
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.
24 Pulls 3 Tags Updated 3 months 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.
11 Pulls 3 Tags Updated 4 months ago