MathForm

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

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},
}