StepFun Prover Preview 32B
StepFun Prover Preview 32B is the larger of StepFun's published proof-search previews. Its declared ancestor is DeepSeek-R1-Distill-Qwen-32B.
Research release
Example settings are not model limits
The card demonstrates generation with a 16,384-token setting and an eight-way tensor-parallel configuration. These are example runtime settings. They do not establish a maximum context window or minimum hardware requirement.StepFun StepFun-Prover-Preview-32B model card
Separate proof search from statement translation
Practical guidance. Begin with a reviewed Lean statement. If the input starts as written mathematics, formalize and check that statement first. This separates mistakes in the problem definition from failures in proof search.
Specifications & access
| Detail | Value and conditions |
|---|---|
| Status | Research release |
| Access | Downloadable |
| Model identifiers | StepFun-Prover-Preview-32B |
| Base model | DeepSeek-R1-Distill-Qwen-32B.StepFun StepFun-Prover-Preview-32B model card |
| License | Apache 2.0 is declared in the model card.StepFun StepFun-Prover-Preview-32B model card |
| Interaction | Repeated proof sketches and Lean 4 REPL feedback.StepFun StepFun-Prover-Preview-32B model card |
Related models
- StepFun Formalizer 32B
StepFun · StepFun Formalizer
A DeepSeek-R1-Distill-Qwen-32B-based model that converts mathematical text into Lean 4 statements.
Launch date not confirmedResearch releaseDownloadable - StepFun Prover Preview 7B
StepFun · StepFun Prover
StepFun Prover Preview 7B is a theorem-proving model derived from DeepSeek-R1-Distill-Qwen-7B.
Launch date not confirmedResearch releaseDownloadable