No official torrent yet — requesting it tells the flock what to host next. You cannot seed a catalog-only page.
Cataloged from openbmb/MathForm-8B
All models by openbmb →
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.
Both servers expose an OpenAI-compatible API at
http://localhost:8000/v1/chat/completions.
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.
This project is licensed under the Apache License 2.0.
import torchfrom 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 serve openbmb/MathForm-8B \ --served-model-name MathForm-8B \ --dtype bfloat16 \ --max-model-len 16384python -m sglang.launch_server \ --model-path openbmb/MathForm-8B \ --served-model-name MathForm-8B \ --dtype bfloat16 \ --context-length 16384@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}, }