StepFun-Formalizer-32B

What is StepFun-Formalizer-32B?

StepFun-Formalizer-32B is an open-weight language model developed by StepFun for mathematical autoformalization. In practical terms, it takes a problem written in ordinary mathematical language and produces a formal statement expressed in Lean 4, a programming language and proof-assistant environment used to represent and verify mathematics.

The distinction between a formalizer and a general-purpose chatbot is important. The model's central task is not open-ended conversation, web research, image understanding, or media generation. It is trained to bridge the gap between informal mathematical descriptions and the precise syntax and definitions required by a formal system. The generated Lean code still needs to be compiled and checked in a suitable Lean environment.

StepFun-Formalizer-32B is the larger model in the StepFun-Formalizer family; StepFun also publishes a 7B version. The 32B checkpoint is distributed through StepFun's official Hugging Face organization under the Apache 2.0 license, making it suitable for local or self-hosted experimentation subject to that license's terms.

Purpose and positioning

The model is positioned for users who need to formalize mathematical statements rather than simply obtain natural-language solutions. For example, an informal request about an algebraic identity, inequality, or theorem can be converted into a Lean 4 proposition with the relevant variables, assumptions, and conclusion represented in formal syntax.

StepFun describes the model as combining formal-language knowledge with reasoning that connects an informal problem to its formal representation. Its ThinkingF training pipeline uses formal mathematical data, synthesized reasoning trajectories, supervised fine-tuning, and reinforcement learning with verifiable rewards. These details are provider and research claims about the training approach, not a guarantee that every generated statement will compile or match the intended theorem.

Technically, the published checkpoint is based on DeepSeek-R1-Distill-Qwen-32B and uses a Qwen2 causal-language-model architecture. That relationship describes the model's starting point and architecture; StepFun-Formalizer-32B remains a distinct specialized release focused on autoformalization.

Key specifications

The 131,072-token figure is the configured context limit, meaning the model can process a very large combined prompt and generation context relative to many smaller language models. It should not be confused with a guaranteed output length. The repository demonstrates a vLLM serving example using max_tokens set to 16,384, but that is an example serving parameter rather than a verified hard maximum output limit for the model. A model-specific maximum output value is therefore not established by the supplied documentation.

Capabilities and supported modalities

StepFun-Formalizer-32B is a text-in, text-out model. Its documented use is to receive textual mathematical prompts and return textual formalizations, often with reasoning traces or intermediate explanation. It does not have documented native image, audio, or video input or output capabilities.

• Mathematical autoformalization: translates informal mathematical problems into Lean 4 statements.
• Formal-language generation: produces code-like mathematical expressions that can be inspected and tested in Lean.
• Reasoning: is specialized toward aligning natural-language mathematical meaning with formal definitions and syntax.
• Coding: is relevant primarily to Lean 4 code generation, rather than broad software engineering.
• Tool use: no native function-calling or tool-use capability is documented for the exact model.
• Structured output: no model-specific JSON-mode or structured-output guarantee is documented.

Although the model generates formal code, generated text is not the same as a verified proof. Lean must compile the result, and a successful compilation process is needed to establish that the formal statement is syntactically and semantically acceptable in the target environment. The model should therefore be treated as an autoformalization assistant, not as a standalone theorem prover.

Published performance

In the StepFun-Formalizer publication, the 32B model achieved a 40.5% BEq@1 score on FormalMATH-Lite and a 26.7% BEq@1 score on ProverBench. BEq evaluates whether a generated formal statement is bidirectionally definitionally equivalent to a reference statement under the evaluation procedure. This is a specialized measure of formalization quality: it is more relevant to the model's intended task than a general chat or coding benchmark, but it should not be read as a general-purpose capability score.

These figures are reported research results, not a promise that the same accuracy will be obtained on every mathematical domain, prompt format, Lean library version, or deployment configuration. In practical use, users should compile generated statements, review definitions and assumptions, and test representative examples.

Deployment, infrastructure, and pricing

The official release is a downloadable checkpoint rather than a metered first-party inference API. StepFun's model documentation describes local inference with Hugging Face Transformers and serving through vLLM or SGLang. The serving documentation also demonstrates OpenAI-compatible server endpoints, but that compatibility refers to the interface exposed by a self-hosted serving layer; it does not establish that StepFun provides a hosted OpenAI-compatible API for this model.

No official input-token or output-token price is specified for StepFun-Formalizer-32B. The financial trade-off is therefore different from that of a hosted API model. Users avoid a published per-request fee, but they must provide the compute, storage, engineering, and operational resources needed to run a 32-billion-parameter checkpoint. Actual speed and cost will depend on hardware, quantization, batching, context length, and serving configuration; the supplied research does not establish a universal tokens-per-second figure.

The model's large context capacity can be useful when a prompt includes lengthy definitions, imported mathematical conventions, or several related statements. However, longer contexts also increase memory and compute requirements, especially in local deployments.

Strengths and limitations

Main strengths

• It is specifically trained for the difficult translation from informal mathematics to formal Lean 4 statements.
• Its 32B scale provides a substantial reasoning and language-model capacity for a specialized research checkpoint.
• The Apache 2.0 open-weight release supports local evaluation, customization, and self-hosted serving.
• The 131,072-token context configuration can accommodate long mathematical prompts and supporting definitions.
• It can be integrated with Transformers, vLLM, or SGLang rather than requiring a proprietary application interface.

Main limitations

• It is not documented as a general-purpose conversational assistant or a replacement for a theorem prover.
• Generated Lean code requires compilation and verification; plausible-looking output may still be incorrect or fail to compile.
• No official hosted inference price, managed API, or guaranteed output-token maximum is documented for the exact model.
• Native image, audio, video, web-search, function-calling, and speech capabilities are not documented.
• There is no published model-specific knowledge-cutoff date in the supplied official materials.
• Running a 32B open-weight model requires users to manage infrastructure and may be slower or more expensive operationally than using a smaller model or hosted service.

When to choose StepFun-Formalizer-32B

Choose StepFun-Formalizer-32B when the central requirement is converting mathematical prose into Lean 4 and you want access to an open-weight model that can be run on your own infrastructure. It is particularly relevant for researchers building autoformalization pipelines, evaluating mathematical reasoning systems, generating candidate theorem statements, or studying how language models interact with proof assistants.

The model is also a reasonable choice when data-control requirements make a self-hosted workflow preferable to sending mathematical material to a managed API. Its long context can help when formalization depends on substantial surrounding definitions or problem context.

A smaller model, such as the 7B member of the same StepFun-Formalizer family, may be more appropriate when memory use, latency, or hardware cost matters more than the capacity of the 32B checkpoint. The larger model is more suitable when the additional reasoning capacity is worth the deployment overhead, but the supplied research does not provide a controlled speed or accuracy comparison sufficient to quantify that trade-off.

A hosted general-purpose model may be more appropriate for ordinary chat, broad software development, web-grounded answers, or multimodal work. A dedicated theorem prover and Lean verification workflow remain necessary when the requirement is proof checking rather than merely generating a candidate formal statement. StepFun-Formalizer-32B occupies the middle step between natural-language mathematics and machine-checked formalization: it helps create the formal artifact, but it does not independently certify every result.

Final assessment

StepFun-Formalizer-32B is best understood as a specialized research and engineering tool for Lean 4 autoformalization. Its most important advantages are task-specific training, an open Apache 2.0 weight release, a large configured context, and support for self-hosted deployment. Its main costs are the infrastructure required to run a 32B model and the need to verify every generated statement in Lean.

For users seeking a managed, multimodal, tool-using assistant, this is the wrong category of model. For users building systems that turn informal mathematics into checkable formal statements, it offers a directly relevant open-weight foundation, provided that generation is paired with compilation, review, and formal verification.