MathForm-8B Translates Natural-Language Math Statements into Lean 4 Formal Proofs

MathForm-8B is an open-source autoformalization model from OpenBMB that translates natural-language mathematical statements into Lean 4. It was trained on FormalVerse through supervised fine-tuning, then reinforcement learning using Lean compilation and semantic-consistency feedback. The model is available on Hugging Face under Apache License 2.0 and can be served with Transformers, vLLM, or SGLang, using a recommended max_new_tokens of 16384.