MathForm — What's That AI

README

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.

📖 Introduction

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.

Average Pass@8 results 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.

News

[2026.08.17]: MathForm paper, code, data and model are released. 🔥🔥🔥

📁 Repository Structure

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

🛠️ Quick Start

Installation

Clone the repository:

git clone https://github.com/OpenBMB/MathForm.git
cd MathForm

Install the Python dependencies:

pip install -r requirements.txt

The experiments use Lean 4.21.0.

Start Kimina Lean Server

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 server

The default endpoint is http://localhost:8000.

Run Data Construction

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/run

Start Lean Explore with run_leanexp_server.sh and add:

LEAN_EXPLORE_URL=http://localhost:9000

The 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.jsonl

Run Evaluation

The 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.sh

Results 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.

🔎 Citation

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

🤝 Acknowledgement

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.

📜 License

This project is licensed under the Apache License 2.0. The bundled third-party
components retain their original license and attribution notices.