stepfun-ai/StepFun-Formalizer-32B

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.