stepfun-ai/StepFun-Formalizer-32B

TEXT GENERATIONConcurrency Cost:2Model Size:32BQuant:FP8Ctx Length:32kPublished:Aug 19, 2025License:apache-2.0Architecture:Transformer0.0K Open Weights Cold

StepFun-Formalizer-32B, developed by stepfun-ai, is a large language model specifically designed for autoformalization, translating natural-language mathematical problems into formal statements in Lean 4. This model integrates formal knowledge with informal-to-formal reasoning capabilities, achieving strong performance on benchmarks like FormalMATH-Lite, ProverBench, and CombiBench. It matches or exceeds prior general-purpose and specialized autoformalization models of comparable scale, making it ideal for advanced mathematical reasoning and formal verification tasks.

Loading preview...

StepFun-Formalizer: Autoformalization with Knowledge-Reasoning Fusion

StepFun-Formalizer is a family of large language models from stepfun-ai, specifically engineered to translate natural-language mathematical problems into formal statements using Lean 4. This model distinguishes itself by fusing formal mathematical knowledge with robust informal-to-formal reasoning capabilities, enabling it to excel in complex autoformalization tasks.

Key Capabilities

  • Natural Language to Lean 4 Translation: Converts mathematical problems described in natural language into precise, verifiable Lean 4 formal statements.
  • Knowledge-Reasoning Fusion: Integrates deep formal knowledge with advanced reasoning to bridge the gap between informal problem descriptions and formal proofs.
  • Strong Benchmark Performance: Achieves competitive or superior results on mainstream autoformalization benchmarks, including FormalMATH-Lite, ProverBench, and CombiBench, as verified by BEq.

Good For

  • Formal Verification: Automating the initial step of formalizing mathematical problems for use with proof assistants like Lean 4.
  • Mathematical Research: Assisting mathematicians and logicians in translating complex informal conjectures into formal systems.
  • Educational Tools: Developing tools that help students understand the formalization process of mathematical concepts.
  • AI for Science: Advancing the capabilities of AI in formal mathematics and automated theorem proving.