MathForm-8B is an autoformalization model that translates natural-language mathematical statements into Lean 4. It is released with the paper MathForm: Scaling Mathematical Autoformalization with Knowledge Retrieval and Verification-Guided Refinement.
The model is trained on FormalVerse through supervised fine-tuning followed by reinforcement learning using Lean compilation and semantic-consistency feedback.
Results
Usage
Transformers
import torch
from transformers import AutoModelForCausalLM, AutoTokenizer
model_id = "openbmb/MathForm-8B"
tokenizer = AutoTokenizer.from_pretrained(model_id)
model = AutoModelForCausalLM.from_pretrained(
model_id, torch_dtype=torch.bfloat16, device_map="auto"
)
prompt = (
"Please convert the following informal math problem to a formal one in Lean 4 with a header. "
"Use the following theorem names: my_favorite_theorem.\n\n"
"Show that for every real number x, x^2 is non-negative."
)
messages = [{"role": "user", "content": prompt}]
text = tokenizer.apply_chat_template(messages, tokenize=False, add_generation_prompt=True)
inputs = tokenizer(text, return_tensors="pt").to(model.device)
outputs = model.generate(
**inputs, max_new_tokens=16384, temperature=0.6, top_p=0.95
)
print(tokenizer.decode(outputs[0][inputs.input_ids.shape[-1]:], skip_special_tokens=True))
vLLM
vllm serve openbmb/MathForm-8B \
--served-model-name MathForm-8B \
--dtype bfloat16 \
--max-model-len 16384
SGLang
python -m sglang.launch_server \
--model-path openbmb/MathForm-8B \
--served-model-name MathForm-8B \
--dtype bfloat16 \
--context-length 16384
Both servers expose an OpenAI-compatible API at
http://localhost:8000/v1/chat/completions.
Recommended Settings
| Setting | Value |
|---|---|
temperature | 0.6 |
top_p | 0.95 |
max_new_tokens | 16384 |
Evaluation
The evaluation pipeline, benchmark files, and Pass@k scripts are available in the MathForm repository. Compilation checks require a running Kimina Lean Server. The experiments use Lean 4.21.0.
License
This project is licensed under the Apache License 2.0.
Citation
@misc{pu2026mathformscalingmathematicalautoformalization,
title={MathForm: Scaling Mathematical Autoformalization with Knowledge Retrieval and Verification-Guided Refinement},
author={Lushi Pu and Weiming Zhang and Xinheng Xie and Zixuan Fu and Bingxiang He and Hengyu Zhao and Hongya Lyu and Xin Li and Jie Zhou and Yudong Wang},
year={2026},
eprint={2608.14221},
archivePrefix={arXiv},
primaryClass={cs.AI},
url={https://arxiv.org/abs/2608.14221},
}