Figure 1: Overview of the MathForm data construction and training pipeline. The system combines Mathlib knowledge retrieval, compilation and semantic verification, and iterative refinement to generate reliable formal data, followed by trajectory reconstruction and training of MathForm-8B.
We introduce MathForm, an autoformalization framework that combines knowledge retrieval from Mathlib with verification-guided iterative refinement. MathForm retrieves relevant definitions and existing formalizations before generation, then uses compiler diagnostics and semantic-consistency feedback to refine generated Lean statements.
Using this framework, we construct FormalVerse, a verified Lean 4 dataset covering diverse mathematical domains and sources. We also train MathForm-8B with supervised fine-tuning followed by reinforcement learning using Lean compilation and semantic-consistency feedback. The released code supports the data construction pipeline and autoformalizer evaluation.
Figure 2: Macro-average Pass@8 (%) across FormalMATH-Lite, ProverBench, CombiBench, FATE-M, FATE-H, and FATE-X among specialized autoformalizers. MathForm-8B achieves the strongest overall performance within this category despite its smaller model size.
src/ Data construction pipeline
evaluation/ Evaluation pipeline and benchmark files
kimina-lean-server/ Lean compilation server source
assets/ Figures used in this README
requirements.txt Python dependencies
- Clone the repository:
git clone https://github.com/OpenBMB/MathForm.git
cd MathForm- Install the Python dependencies:
pip install -r requirements.txtThe experiments use Lean 4.21.0.
The evaluation and data-construction pipelines require a running Kimina Lean Server for compilation checks.
cd kimina-lean-server
cp .env.template .env
bash setup.sh
pip install -r requirements.txt
pip install .
prisma generate
python -m serverThe default endpoint is http://localhost:8000.
The input is a JSONL file containing a natural-language statement in a field
such as statement or informal_statement.
cd src
API_URL=https://api.example.com/v1/chat/completions \
API_KEY="$API_KEY" \
BASE_MODEL_NAME=[GENERATION_MODEL] \
JUDGE_MODEL_NAME=[JUDGE_MODEL] \
LEAN_SERVER_URL=http://localhost:8000 \
bash run.sh path/to/input.jsonl output/runStart Lean Explore with run_leanexp_server.sh and add:
LEAN_EXPLORE_URL=http://localhost:9000The generated files include success.jsonl, failed.jsonl, and
pipeline.log. Successful samples can be normalized and filtered with:
python postprocess.py normalize \
--input output/run/success.jsonl \
--output output/run/normalized.jsonl
python postprocess.py filter \
--input output/run/normalized.jsonl \
--output output/run/filtered.jsonlThe default evaluation uses the benchmark files under
evaluation/benchmarks/.
cd evaluation
EVAL_API_BASE_URL=https://api.example.com/v1 \
EVAL_API_MODEL=[EVALUATION_MODEL] \
JUDGE_API_BASE_URL=https://api.example.com/v1 \
JUDGE_API_MODEL=[JUDGE_MODEL] \
API_KEY="$API_KEY" \
bash run.shResults are written to evaluation/output/:
predictions.jsonl Generated Lean candidates
results.jsonl Compilation and judge results
results.compile.jsonl Compilation cache
results.summary.json Pass@k summary
To evaluate another benchmark or change the number of samples, set
DATASET_PATHS or NUM_SAMPLES before running run.sh.
If you find this repository useful, please cite our paper:
@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},
}This repository builds on the following open-source projects:
- Kimina Lean Server for Lean compilation checks.
- Lean Explore for retrieval.
The evaluation uses the following benchmarks:
Part of the informal problems used to build FormalVerse are drawn from the following open collections:
We thank the authors and contributors of these projects.
This project is licensed under the Apache License 2.0. The bundled third-party components retain their original license and attribution notices.