stepfun-ai/StepFun-Prover-Preview-32B
TEXT GENERATIONConcurrency Cost:2Model Size:32BQuant:FP8Ctx Length:32kPublished:Aug 13, 2025License:apache-2.0Architecture:Transformer0.0K Open Weights Warm
StepFun-Prover-Preview-32B is a 32 billion parameter theorem proving model developed by the StepFun Team. This model is specifically designed to iteratively refine proof sketches by interacting with Lean4. It achieves a 70.0% accuracy with Pass@1 on the MiniF2F-test benchmark, making it highly effective for formal theorem proving tasks. Its primary strength lies in its ability to generate and validate mathematical proofs.
Loading preview...
StepFun-Prover-Preview-32B Overview
StepFun-Prover-Preview-32B is a specialized 32 billion parameter language model developed by the StepFun Team, focusing on automated theorem proving. Its core capability is to assist in the creation and validation of mathematical proofs within the Lean 4 formal verification system.
Key Capabilities
- Interactive Proof Generation: The model can iteratively refine proof sketches by interacting with a Lean 4 environment, receiving feedback to guide its progress.
- High Accuracy in Formal Proofs: It demonstrates strong performance in theorem proving, achieving 70.0% accuracy with Pass@1 on the MiniF2F-test benchmark.
- Lean 4 Integration: Designed to work seamlessly with Lean 4, utilizing its REPL for real-time validation of partial solutions.
Good For
- Formal Verification: Researchers and developers working on formal verification of mathematical theorems or software.
- Automated Theorem Proving: Tasks requiring the generation and validation of complex mathematical proofs.
- Lean 4 Development: Assisting in the construction of Lean 4 proofs, particularly for challenging problems.