What is StepFun-Prover-Preview-7B?
StepFun-Prover-Preview-7B is an open-weight language model developed by StepFun for formal mathematical theorem proving. Its output is text, but the important kind of text is Lean 4 proof code: a machine-checkable description of how a theorem follows from its assumptions and available definitions.
The model is based on DeepSeek-R1-Distill-Qwen-7B and is fine-tuned for proof-generation tasks. The published model repository describes it as an approximately 8-billion-parameter BF16 model. BF16 is a reduced-precision numerical format commonly used to reduce memory requirements during inference, although the supplied research does not specify the exact hardware needed to run this checkpoint.
The “Preview” designation is significant. This is a research-oriented release intended for experimentation with formal reasoning and verifier-guided generation, rather than a broadly supported commercial assistant. It is publicly available through StepFun’s model repositories and is released under the Apache License 2.0.
How the Lean 4 proof workflow works
StepFun-Prover-Preview-7B is designed around an interaction between the model and Lean 4. Lean 4 is a programming language and proof assistant that can check whether a proposed formal proof is valid. Instead of treating the model’s first response as final, the workflow can submit a generated proof sketch to Lean 4 and use the resulting errors or verification feedback to guide another attempt.
- Proof generation: the model receives a formal theorem or a related proof task and proposes Lean 4 code.
- Verification: the proposed code is evaluated in a Lean 4 environment.
- Revision: the model uses the environment’s feedback to correct or extend the proof.
- Completion: the process continues until Lean 4 accepts the proof or the available generation budget is exhausted.
This workflow is the model’s defining capability. It is not the same as verified native function calling in a general API. The research identifies tool use as support for the Lean 4 interaction protocol, not as evidence that the model offers standard OpenAI-compatible function calling or a general-purpose agent interface.
Main strengths
Formal, machine-checkable output
The model targets proofs that can be checked by Lean 4 rather than relying only on plausible natural-language explanations. This is valuable when correctness must be established by a formal system. A generated proof that Lean 4 accepts has passed the verifier’s checks for the relevant theorem, imports, definitions, and proof steps.
Verifier-guided reasoning
Many language models can produce a promising proof idea but fail on syntax, missing lemmas, type mismatches, or invalid intermediate steps. StepFun-Prover-Preview-7B is designed to address those issues through repeated interaction with Lean 4. The feedback loop gives the model concrete information about why a candidate proof failed, making the system more suitable for iterative proof search than a one-shot text-generation approach.
Open-weight research access
The checkpoint is publicly distributed rather than available only through a paid hosted endpoint. Researchers and developers can inspect the published model materials and build their own local or experimental inference workflow. The Apache 2.0 license also makes the release more permissive for many forms of use than a closed, provider-controlled API, subject to the license and the user’s own deployment obligations.
Reported theorem-proving results
StepFun reports 66.0% Pass@1 on the MiniF2F-test benchmark in its repository evaluation. Pass@1 measures whether the first sampled attempt succeeds under the stated evaluation procedure. The associated technical report gives a different 64.2% result for the 7B model under another evaluation presentation. These numbers should not be treated as directly interchangeable: the evaluation setup, sampling conditions, or reporting methodology may differ. They are provider or research-report results, not an independent editorial rating.
Technical specifications and limits
| Specification | Documented information |
|---|---|
| Provider | StepFun |
| Model family | StepFun-Prover Preview |
| Approximate size | Approximately 8 billion parameters |
| Model format | BF16 |
| Base model | DeepSeek-R1-Distill-Qwen-7B |
| Primary output | Text, especially Lean 4 proof code |
| Formal reasoning environment | Lean 4 |
| Published context figure | 20,480 tokens in the StepFun evaluation setup |
| Published generation example | 16,384 maximum output tokens in the vLLM example |
| License | Apache License 2.0 |
The 20,480-token context figure should be interpreted carefully. The supplied research identifies it with StepFun’s evaluation setup, not with a separately documented hosted API limit. Likewise, the 16,384-token value comes from the published vLLM example and should not automatically be treated as a universal maximum for every inference engine or deployment configuration. Available memory, inference software, prompt length, and generation settings can affect practical limits.
Modalities and supported capabilities
StepFun-Prover-Preview-7B is a text-only model. It accepts text input and produces text output; there is no supplied evidence of image, audio, video, speech, music, or other direct non-text input or output. It is therefore not intended for multimodal applications.
Its reasoning capability is specialized rather than broad. The model’s central task is formal proof generation and refinement, particularly in Lean 4. It can be useful for mathematical reasoning when the problem can be represented in the supported formal environment, but the research does not establish that it is a top choice for general conversation, unrestricted mathematics, factual question answering, or long-form writing.
The model can generate code in the specific sense that Lean 4 proofs are programs or formal code. The supplied information does not support describing it as a general software-engineering model or as a model with broad programming-language coverage. Similarly, its documented tool interaction is Lean 4 verification, not a general tool registry or standard function-calling API.
Speed, cost, and deployment trade-offs
The model’s open-weight format can avoid per-token hosted API charges, but it does not make inference free. Users must provide compatible compute, storage, an inference stack, and a Lean 4 environment. The research identifies no official token pricing and no first-party hosted commercial API endpoint for this model.
Its iterative proof workflow can also be slower than one-shot text generation. A single theorem may require multiple model generations and Lean 4 verification passes. This extra work is the source of an important benefit—machine-checkable feedback—but it increases latency and operational complexity compared with asking a general language model for an informal proof explanation.
For cost-sensitive experimentation, a local open-weight checkpoint may be attractive when the user already has suitable infrastructure. For users who need predictable latency, managed scaling, service-level support, or a conventional API, this model is a weaker fit because those offerings were not identified in the supplied research.
Best use cases
- Generating Lean 4 proof sketches for formal mathematics.
- Iteratively repairing proof attempts using compiler or verifier feedback.
- Research on language models that interact with external verifiers.
- Experiments with theorem-proving search, proof refinement, and tool-integrated reasoning.
- Benchmarking open-weight models on formal mathematics tasks such as MiniF2F-style evaluation.
A practical user should expect to work with theorem statements, Lean 4 syntax, the relevant environment, and the model’s inference code. The model is most useful when success is defined by whether Lean 4 accepts the resulting proof, rather than by whether the explanation sounds mathematically convincing to a human reader.
When to choose this model
Choose StepFun-Prover-Preview-7B when you specifically need an open-weight model for Lean 4 theorem proving and are prepared to run or integrate the verifier loop yourself. It is particularly appropriate for research and prototyping where access to model weights, reproducibility, and experimentation matter more than hosted convenience.
Choose another type of model when you need a general-purpose assistant, multimodal input or output, image or audio generation, a managed commercial endpoint, or standard function-calling support. A general coding model may be more suitable for ordinary application development, while a hosted reasoning service may be preferable when infrastructure and latency are more important than local control. The supplied research does not identify a specific sibling model that can be compared directly on the same terms, so those alternatives should be evaluated by their actual Lean 4 support rather than by general model branding.
Limitations to keep in mind
The model is specialized and should not be assumed to provide broad production support. The “Preview” status, lack of identified official API pricing, and reliance on a local Lean 4 workflow make deployment less turnkey than using a conventional hosted language model. The benchmark results are also tied to their respective evaluation settings and should not be interpreted as a guarantee that every theorem will be solved on the first attempt.
Finally, the supplied sources do not specify a knowledge-cutoff date, fine-tuning service, caching service, batch API, or separate structured-output mode. Those features should therefore be treated as undocumented rather than available. Its documented value lies in open-weight, verifier-guided Lean 4 proof generation—not in a broad catalog of general API features.